Merge branch 'v8.5'

2 files changed, 91 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4363.v b/test-suite/bugs/closed/4363.v
new file mode 100644
index 0000000000..9895548c1d
--- /dev/null
+++ b/test-suite/bugs/closed/4363.v
@@ -0,0 +1,9 @@
+Set Printing Universes.
+Definition foo : Type.
+Proof.
+  assert (H : Set) by abstract (assert Type by abstract exact Type using bar; exact nat).
+  exact bar.
+Defined. (* Toplevel input, characters 0-8:
+Error:
+The term "(fun _ : Set => bar) foo_subproof" has type
+"Type@{Top.2}" while it is expected to have type "Type@{Top.1}". *)
diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v
new file mode 100644
index 0000000000..dfdeff82ff
--- /dev/null
+++ b/test-suite/success/extraction_impl.v
@@ -0,0 +1,82 @@
+
+(** Examples of extraction with manually-declared implicit arguments *)
+
+(** NB: we should someday check the produced code instead of
+    simply running the commands. *)
+
+(** Bug #4243, part 1 *)
+
+Inductive dnat : nat -> Type :=
+| d0 : dnat 0
+| ds : forall n m, n = m -> dnat n ->  dnat (S n).
+
+Extraction Implicit ds [m].
+
+Lemma dnat_nat: forall n, dnat n -> nat.
+Proof.
+  intros n d.
+  induction d as [| n m Heq d IHn].
+  exact 0. exact (S IHn).
+Defined.
+
+Recursive Extraction dnat_nat.
+
+Extraction Implicit dnat_nat [n].
+Recursive Extraction dnat_nat.
+
+(** Same, with a Fixpoint *)
+
+Fixpoint dnat_nat' n (d:dnat n) :=
+ match d with
+ | d0 => 0
+ | ds n m _ d => S (dnat_nat' n d)
+ end.
+
+Recursive Extraction dnat_nat'.
+
+Extraction Implicit dnat_nat' [n].
+Recursive Extraction dnat_nat'.
+
+(** Bug #4243, part 2 *)
+
+Inductive enat: nat -> Type :=
+  e0: enat 0
+| es: forall n, enat n -> enat (S n).
+
+Lemma enat_nat: forall n, enat n -> nat.
+Proof.
+  intros n e.
+  induction e as [| n e IHe].
+  exact (O).
+  exact (S IHe).
+Defined.
+
+Extraction Implicit es [n].
+Extraction Implicit enat_nat [n].
+Recursive Extraction enat_nat.
+
+(** Same, with a Fixpoint *)
+
+Fixpoint enat_nat' n (e:enat n) : nat :=
+ match e with
+ | e0 => 0
+ | es n e => S (enat_nat' n e)
+ end.
+
+Extraction Implicit enat_nat' [n].
+Recursive Extraction enat_nat'.
+
+(** Bug #4228 *)
+
+Module Food.
+Inductive Course :=
+| main:    nat -> Course
+| dessert: nat -> Course.
+
+Inductive Meal : Course -> Type :=
+| one_course : forall n:nat, Meal (main n)
+| two_course : forall n m, Meal (main n) -> Meal (dessert m).
+Extraction Implicit two_course [n].
+End Food.
+
+Recursive Extraction Food.Meal.