From 3c81c6c3b595ef06e0c01e51775aa0118f44e421 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 11 Dec 2015 17:59:42 +0100
Subject: Univs: Fix bug #4363, nested abstract.

---
 test-suite/bugs/closed/4363.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/4363.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4363.v b/test-suite/bugs/closed/4363.v
new file mode 100644
index 0000000000..75a9c9a041
--- /dev/null
+++ b/test-suite/bugs/closed/4363.v
@@ -0,0 +1,7 @@
+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:
\ No newline at end of file
-- 
cgit v1.2.3


From 9329cb508f336b48a2bf2e699886546158b6b4d8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 14 Dec 2015 11:14:45 +0100
Subject: Test file for #4363 was not complete.

---
 test-suite/bugs/closed/4363.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4363.v b/test-suite/bugs/closed/4363.v
index 75a9c9a041..9895548c1d 100644
--- a/test-suite/bugs/closed/4363.v
+++ b/test-suite/bugs/closed/4363.v
@@ -4,4 +4,6 @@ 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:
\ No newline at end of file
+Error:
+The term "(fun _ : Set => bar) foo_subproof" has type
+"Type@{Top.2}" while it is expected to have type "Type@{Top.1}". *)
-- 
cgit v1.2.3


From 6ab322a9b0725aaa9fa6f457db061f2635598fe9 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 14 Dec 2015 20:13:45 +0100
Subject: A test file for Extraction Implicit (including bugs #4243 and #4228)

---
 test-suite/success/extraction_impl.v | 82 ++++++++++++++++++++++++++++++++++++
 1 file changed, 82 insertions(+)
 create mode 100644 test-suite/success/extraction_impl.v

(limited to 'test-suite')

diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v
new file mode 100644
index 0000000000..a72715f292
--- /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.
-- 
cgit v1.2.3


From c3aa4c065fac0e37d67ca001aec47b1c2138e648 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 14 Dec 2015 20:29:45 +0100
Subject: extraction_impl.v: fix a typo

---
 test-suite/success/extraction_impl.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v
index a72715f292..dfdeff82ff 100644
--- a/test-suite/success/extraction_impl.v
+++ b/test-suite/success/extraction_impl.v
@@ -64,7 +64,7 @@ Fixpoint enat_nat' n (e:enat n) : nat :=
  end.
 
 Extraction Implicit enat_nat' [n].
-Recursive Extraction enat_nat.
+Recursive Extraction enat_nat'.
 
 (** Bug #4228 *)
 
-- 
cgit v1.2.3