Merge PR #10577: Fix #7348: extraction of dependent record projections

Reviewed-by: Zimmi48
Reviewed-by: maximedenes

2 files changed, 70 insertions, 0 deletions

diff --git a/test-suite/output/bug7348.out b/test-suite/output/bug7348.out
new file mode 100644
index 0000000000..325ee95ae2
--- /dev/null
+++ b/test-suite/output/bug7348.out
@@ -0,0 +1,45 @@
+Extracted code successfully compiled
+
+type __ = Obj.t
+
+type unit0 =
+| Tt
+
+type bool =
+| True
+| False
+
+module Case1 =
+ struct
+  type coq_rec = { f : bool }
+
+  (** val f : bool -> coq_rec -> bool **)
+
+  let f _ r =
+    r.f
+
+  (** val silly : bool -> coq_rec -> __ **)
+
+  let silly x b =
+    match x with
+    | True -> Obj.magic b.f
+    | False -> Obj.magic Tt
+ end
+
+module Case2 =
+ struct
+  type coq_rec = { f : (bool -> bool) }
+
+  (** val f : bool -> coq_rec -> bool -> bool **)
+
+  let f _ r =
+    r.f
+
+  (** val silly : bool -> coq_rec -> __ **)
+
+  let silly x b =
+    match x with
+    | True -> Obj.magic b.f False
+    | False -> Obj.magic Tt
+ end
+
diff --git a/test-suite/output/bug7348.v b/test-suite/output/bug7348.v
new file mode 100644
index 0000000000..782b27ce96
--- /dev/null
+++ b/test-suite/output/bug7348.v
@@ -0,0 +1,25 @@
+Require Extraction.
+
+Extraction Language OCaml.
+Set Extraction KeepSingleton.
+
+Module Case1.
+
+Record rec (x : bool) := { f : bool }.
+
+Definition silly x (b : rec x) :=
+  if x return (if x then bool else unit) then f x b else tt.
+
+End Case1.
+
+Module Case2.
+
+Record rec (x : bool) := { f : bool -> bool }.
+
+Definition silly x (b : rec x) :=
+  if x return (if x then bool else unit) then f x b false else tt.
+
+End Case2.
+
+Extraction TestCompile Case1.silly Case2.silly.
+Recursive Extraction Case1.silly Case2.silly.