From 87d6f6c7c90bf7b427397d6bd2e2c70d610678e3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jul 2023 14:57:51 +0200
Subject: Reorganize the Lean tests

---
 compiler/ExtractBase.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'compiler/ExtractBase.ml')

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,
-- 
cgit v1.2.3