Reorganize the Lean tests

1 files changed, 10 insertions, 0 deletions

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 0a5d7df2..14ce4119 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -539,6 +539,16 @@ type extraction_ctx = {
           use it.
           Also see {!names_map.opaque_ids}.
        *)
+  use_dep_ite : bool;
+      (** For Lean: do we use dependent-if then else expressions?
+
+          Example:
+          {[
+            if h: b then ... else ...
+            -- ^^
+            -- makes the if then else dependent
+          ]}
+        *)
 }
 
 (** Debugging function, used when communicating name collisions to the user,