From f713e6c195d1de177b43cab7c2902f5160f6af9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Mar 2017 02:18:53 +0100
Subject: A fix to #5414 (ident bound by ltac names now known for "match").

Also taking into account a name in the return clause and in the
indices.

Note the double meaning ``bound as a term to match'' and ``binding in
the "as" clause'' when the term to match is a variable for all of
"match", "if" and "let".
---
 test-suite/bugs/closed/5414.v | 12 +++++++++
 test-suite/output/Cases.out   | 46 +++++++++++++++++++++++++++++++
 test-suite/output/Cases.v     | 63 +++++++++++++++++++++++++++++++++++++++++++
 test-suite/success/Case19.v   | 19 +++++++++++++
 4 files changed, 140 insertions(+)
 create mode 100644 test-suite/bugs/closed/5414.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5414.v b/test-suite/bugs/closed/5414.v
new file mode 100644
index 0000000000..2522a274fb
--- /dev/null
+++ b/test-suite/bugs/closed/5414.v
@@ -0,0 +1,12 @@
+(* Use of idents bound to ltac names in a "match" *)
+
+Definition foo : Type.
+Proof.
+  let x := fresh "a" in
+  refine (forall k : nat * nat, let '(x, _) := k in (_ : Type)).
+  exact (a = a).
+Defined.
+Goal foo.
+intros k. elim k. (* elim because elim keeps names *)
+intros.
+Check a. (* We check that the name is "a" *)
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index f064dfe763..97fa8e2542 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -80,3 +80,49 @@ fun '(D n m p q) => n + m + p + q
      : J -> nat
 The command has indeed failed with message:
 The constructor D (in type J) expects 3 arguments.
+lem1 = 
+fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
+     : forall k : nat * nat, k = k
+lem2 = 
+fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
+     : forall k : bool, k = k
+
+Argument scope is [bool_scope]
+lem3 = 
+fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
+     : forall k : nat * nat, k = k
+1 subgoal
+  
+  x : nat
+  n, n0 := match x + 0 with
+           | 0 => 0
+           | S _ => 0
+           end : nat
+  e,
+  e0 := match x + 0 as y return (y = y) with
+        | 0 => eq_refl
+        | S n => eq_refl
+        end : x + 0 = x + 0
+  n1, n2 := match x with
+            | 0 => 0
+            | S _ => 0
+            end : nat
+  e1, e2 := match x return (x = x) with
+            | 0 => eq_refl
+            | S n => eq_refl
+            end : x = x
+  ============================
+  x + 0 = 0
+1 subgoal
+  
+  p : nat
+  a,
+  a0 := match eq_refl as y in (_ = e) return (y = y /\ e = e) with
+        | eq_refl => conj eq_refl eq_refl
+        end : eq_refl = eq_refl /\ p = p
+  a1,
+  a2 := match eq_refl in (_ = e) return (p = p /\ e = e) with
+        | eq_refl => conj eq_refl eq_refl
+        end : p = p /\ p = p
+  ============================
+  eq_refl = eq_refl
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 6a4fd007df..17fee3303d 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -121,3 +121,66 @@ Check fun x => let '(D n m p q) := x in n+m+p+q.
 (* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *)
 
 Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p.
+
+(* Test use of idents bound to ltac names in a "match" *)
+
+Lemma lem1 : forall k, k=k :>nat * nat.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k : nat * nat => match k as x return x = x with (y,z) => eq_refl end).
+Qed.
+Print lem1.
+
+Lemma lem2 : forall k, k=k :> bool.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k => if k as x return x = x then eq_refl else eq_refl).
+Qed.
+Print lem2.
+
+Lemma lem3 : forall k, k=k :>nat * nat.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k : nat * nat => let (y,z) as x return x = x := k in eq_refl).
+Qed.
+Print lem3.
+
+Lemma lem4 x : x+0=0.
+match goal with |- ?y = _ => pose (match y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y = _ => pose (match y as y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y + _ = _ => pose (match y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+Show.
+
+Lemma lem5 (p:nat) : eq_refl p = eq_refl p.
+let y := fresh "n" in (* Checking that y is hidden *)
+  let z := fresh "e" in (* Checking that z is hidden *)
+  match goal with
+  |- ?y = _ => pose (match y as y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let y := fresh "n" in
+  let z := fresh "e" in
+  match goal with
+  |- ?y = _ => pose (match y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let y := fresh "n" in
+  let z := fresh "e" in
+  match goal with
+  |- eq_refl ?y = _ => pose (match eq_refl y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let p := fresh "p" in
+  let z := fresh "e" in
+  match goal with
+  |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+Show.
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v
index e59828defe..ce98879a5f 100644
--- a/test-suite/success/Case19.v
+++ b/test-suite/success/Case19.v
@@ -17,3 +17,22 @@ Fail exists (fun x =>
         with
         | eq_refl => eq_refl
         end).
+Abort.
+
+(* Some tests with ltac matching on building "if" and "let" *)
+
+Goal forall b c d, (if negb b then c else d) = 0.
+intros.
+match goal with
+|- (if ?b then ?c else ?d) = 0 => transitivity (if b then d else c)
+end.
+Abort.
+
+Definition swap {A} {B} '((x,y):A*B) := (y,x).
+
+Goal forall p, (let '(x,y) := swap p in x + y) = 0.
+intros.
+match goal with
+|- (let '(x,y) := ?p in x + y) = 0 => transitivity (let (x,y) := p in x+y)
+end.
+Abort.
-- 
cgit v1.2.3


From 7e0f61eb7cd16b2f2e58ce7ca18992fde7ac9aea Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Jun 2017 11:34:11 +0200
Subject: A stronger test that #use"include";; works well.

---
 test-suite/misc/printers.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh
index c822d0eb37..28e7dc362f 100755
--- a/test-suite/misc/printers.sh
+++ b/test-suite/misc/printers.sh
@@ -1,3 +1,3 @@
-printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep Unbound
+printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound"
 if [ $? = 0 ]; then exit 1; else exit 0; fi
 
-- 
cgit v1.2.3


From bcaf9af83363f3e1a1c588271e5038984ee1760b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sat, 8 Apr 2017 07:04:56 +0200
Subject: Remove support for Coq 8.4.

---
 test-suite/bugs/closed/4394.v | 19 ----------------
 test-suite/bugs/closed/4400.v | 19 ----------------
 test-suite/bugs/closed/4656.v |  4 ----
 test-suite/bugs/closed/4727.v | 10 ---------
 test-suite/bugs/closed/4733.v | 52 -------------------------------------------
 test-suite/bugs/opened/4803.v | 48 ---------------------------------------
 test-suite/success/Compat84.v | 19 ----------------
 7 files changed, 171 deletions(-)
 delete mode 100644 test-suite/bugs/closed/4394.v
 delete mode 100644 test-suite/bugs/closed/4400.v
 delete mode 100644 test-suite/bugs/closed/4656.v
 delete mode 100644 test-suite/bugs/closed/4727.v
 delete mode 100644 test-suite/bugs/closed/4733.v
 delete mode 100644 test-suite/bugs/opened/4803.v
 delete mode 100644 test-suite/success/Compat84.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v
deleted file mode 100644
index 1ad81345db..0000000000
--- a/test-suite/bugs/closed/4394.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-
-Require Import Equality List.
-Inductive Foo (I : Type -> Type) (A : Type) : Type :=
-| foo (B : Type) : A -> I B -> Foo I A.
-Definition Family := Type -> Type.
-Definition FooToo : Family -> Family := Foo.
-Definition optionize (I : Type -> Type) (A : Type) := option (I A).
-Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A.
-Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
-Definition barRec : Rec (optionize id) := {| rec := bar id |}.
-Inductive Empty {T} : T -> Prop := .
-Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) :
-  Empty (a, b) -> False.
-Proof.
-  intro e.
-  dependent induction e.
-Qed.
-
diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v
deleted file mode 100644
index a89cf0cbc3..0000000000
--- a/test-suite/bugs/closed/4400.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *)
-Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality.
-Set Printing Universes.
-Inductive Foo (I : Type -> Type) (A : Type) : Type :=
-| foo (B : Type) : A -> I B -> Foo I A.
-Definition Family := Type -> Type.
-Definition FooToo : Family -> Family := Foo.
-Definition optionize (I : Type -> Type) (A : Type) := option (I A).
-Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A.
-Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
-Definition barRec : Rec (optionize id) := {| rec := bar id |}.
-Inductive Empty {T} : T -> Prop := .
-Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family)
-nil)) (b : unit) :
-  Empty (a, b) -> False.
-Proof.
-  intro e.
-  dependent induction e.
-Qed.
diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v
deleted file mode 100644
index a59eed2c86..0000000000
--- a/test-suite/bugs/closed/4656.v
+++ /dev/null
@@ -1,4 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-Goal True.
-  constructor 1.
-Qed.
diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v
deleted file mode 100644
index cfb4548d2c..0000000000
--- a/test-suite/bugs/closed/4727.v
+++ /dev/null
@@ -1,10 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0),
-    (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) ->
-    o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False.
-Proof.
-  clear; intros ???????? inj H0 H1 H2.
-  destruct H2; intuition subst.
-  eapply inj in H1; [ | eauto ].
-  progress subst. (* should succeed, used to not succeed *)
-Abort.
diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v
deleted file mode 100644
index a90abd71cf..0000000000
--- a/test-suite/bugs/closed/4733.v
+++ /dev/null
@@ -1,52 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
-Require Import Coq.Lists.List.
-Require Import Coq.Vectors.Vector.
-Import ListNotations.
-Import VectorNotations.
-Set Implicit Arguments.
-Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
-Arguments mynil {_}, _.
-
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Delimit Scope vector_scope with vector.
-
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x mynil) : mylist_scope.
-Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
-
-(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
-
-Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
-(* Now these all work, but not so in 8.4.  If we get the ability to remove notations, this section can also just be removed. *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
deleted file mode 100644
index 4541f13d01..0000000000
--- a/test-suite/bugs/opened/4803.v
+++ /dev/null
@@ -1,48 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
-Require Import Coq.Lists.List.
-Require Import Coq.Vectors.Vector.
-Import ListNotations.
-Import VectorNotations.
-Set Implicit Arguments.
-Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
-Arguments mynil {_}, _.
-
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Delimit Scope vector_scope with vector.
-
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x mynil) : mylist_scope.
-Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
-
-(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
-
-(** Now check that we can add and then remove notations from the parser *)
-(* We should be able to stick some vernacular here to remove [] from the parser *)
-Fail Remove Notation "[]".
-Goal True.
-  (* This should not be a syntax error; before moving this file to closed, uncomment this line. *)
-  (* idtac; []. *)
-  constructor.
-Qed.
-
-Check { _ : _ & _ }.
-Reserved Infix "&" (at level 0).
-Fail Remove Infix "&".
-(* Check { _ : _ & _ }. *)
diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
deleted file mode 100644
index 732a024fc1..0000000000
--- a/test-suite/success/Compat84.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-
-Goal True.
-  solve [ constructor 1 ]. Undo.
-  solve [ econstructor 1 ]. Undo.
-  solve [ constructor ]. Undo.
-  solve [ econstructor ]. Undo.
-  solve [ constructor (fail) ]. Undo.
-  solve [ econstructor (fail) ]. Undo.
-  split.
-Qed.
-
-Goal False \/ True.
-  solve [ constructor (constructor) ]. Undo.
-  solve [ econstructor (econstructor) ]. Undo.
-  solve [ constructor 2; constructor ]. Undo.
-  solve [ econstructor 2; econstructor ]. Undo.
-  right; esplit.
-Qed.
-- 
cgit v1.2.3


From d038839a32978548051573286e22462d68d42ee6 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 26 Apr 2016 17:30:30 +0200
Subject: Constrexpr.Numeral stays uninterpreted (string+sign instead of
 BigInt.t)

 This string contains the base-10 representation of the number (big endian)

 Note that some inner parsing stuff still uses bigints, see egramcoq.ml
---
 test-suite/bugs/closed/3036.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3036.v b/test-suite/bugs/closed/3036.v
index 451bec9b20..3b57310d6e 100644
--- a/test-suite/bugs/closed/3036.v
+++ b/test-suite/bugs/closed/3036.v
@@ -15,11 +15,11 @@ Definition perm := Qc.
 Locate Qle_bool.
 
 Definition compatibleb (p1 p2 : perm) : bool :=
-let p1pos := Qle_bool 00 p1 in
-  let p2pos := Qle_bool 00 p2 in
+let p1pos := Qle_bool 0 p1 in
+  let p2pos := Qle_bool 0 p2 in
     negb (
          (p1pos && p2pos)
-      || ((p1pos || p2pos) && (negb (Qle_bool 00 ((p1 + p2)%Qc)))))%Qc.
+      || ((p1pos || p2pos) && (negb (Qle_bool 0 ((p1 + p2)%Qc)))))%Qc.
 
 Definition compatible (p1 p2 : perm) := compatibleb p1 p2 = true.
 
-- 
cgit v1.2.3


From 27c8e30fad95d887b698b0e3fa563644c293b033 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Thu, 23 Jun 2016 15:07:02 +0200
Subject: Prelude : no more autoload of plugins extraction and recdef

 The user now has to manually load them, respectively via:
   Require Extraction
   Require Import FunInd

 The "Import" in the case of FunInd is to ensure that the
 tactics functional induction and functional inversion are indeed
 in scope.

 Note that the Recdef.v file is still there as well (it contains
 complements used when doing Function with measures), and it also
 triggers a load of FunInd.v.

 This change is correctly documented in the refman, and the test-suite
 has been adapted.
---
 test-suite/bugs/closed/2141.v              | 1 +
 test-suite/bugs/closed/3287.v              | 2 ++
 test-suite/bugs/closed/3923.v              | 2 ++
 test-suite/bugs/closed/4616.v              | 2 ++
 test-suite/bugs/closed/4710.v              | 2 ++
 test-suite/bugs/closed/5372.v              | 1 +
 test-suite/ide/blocking-futures.fake       | 1 +
 test-suite/output/Extraction_matchs_2413.v | 2 ++
 test-suite/success/Funind.v                | 2 ++
 test-suite/success/RecTutorial.v           | 1 +
 test-suite/success/extraction.v            | 1 +
 test-suite/success/extraction_dep.v        | 2 ++
 test-suite/success/extraction_impl.v       | 2 ++
 test-suite/success/extraction_polyprop.v   | 2 ++
 test-suite/success/primitiveproj.v         | 2 ++
 15 files changed, 25 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2141.v b/test-suite/bugs/closed/2141.v
index 941ae530fd..098a7e9e72 100644
--- a/test-suite/bugs/closed/2141.v
+++ b/test-suite/bugs/closed/2141.v
@@ -1,3 +1,4 @@
+Require Coq.extraction.Extraction.
 Require Import FSetList.
 Require Import OrderedTypeEx.
 
diff --git a/test-suite/bugs/closed/3287.v b/test-suite/bugs/closed/3287.v
index 7c78131252..1b758acd73 100644
--- a/test-suite/bugs/closed/3287.v
+++ b/test-suite/bugs/closed/3287.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Module Foo.
 (* Definition foo := (I,I). *)
 Definition bar := true.
diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v
index 0aa029e73d..2fb0a5439a 100644
--- a/test-suite/bugs/closed/3923.v
+++ b/test-suite/bugs/closed/3923.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Module Type TRIVIAL.
 Parameter t:Type.
 End TRIVIAL.
diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v
index c862f82067..a59975dbcf 100644
--- a/test-suite/bugs/closed/4616.v
+++ b/test-suite/bugs/closed/4616.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Set Primitive Projections.
 Record Foo' := Foo { foo : Type }.
 Axiom f : forall t : Foo', foo t.
diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v
index fdc8501099..5d8ca330ac 100644
--- a/test-suite/bugs/closed/4710.v
+++ b/test-suite/bugs/closed/4710.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Set Primitive Projections.
 Record Foo' := Foo { foo : nat }.
 Extraction foo.
diff --git a/test-suite/bugs/closed/5372.v b/test-suite/bugs/closed/5372.v
index 2dc78d4c7f..e60244cd1d 100644
--- a/test-suite/bugs/closed/5372.v
+++ b/test-suite/bugs/closed/5372.v
@@ -1,4 +1,5 @@
 (* coq bug 5372: https://coq.inria.fr/bugs/show_bug.cgi?id=5372 *)
+Require Import FunInd.
 Function odd (n:nat) :=
   match n with
   | 0 => false
diff --git a/test-suite/ide/blocking-futures.fake b/test-suite/ide/blocking-futures.fake
index b63f09bcfc..541fb798c0 100644
--- a/test-suite/ide/blocking-futures.fake
+++ b/test-suite/ide/blocking-futures.fake
@@ -4,6 +4,7 @@
 # Extraction will force the future computation, assert it is blocking
 # Example courtesy of Jonathan (jonikelee)
 #
+ADD { Require Coq.extraction.Extraction. }
 ADD { Require Import List. }
 ADD { Import ListNotations. }
 ADD { Definition myrev{A}(l : list A) : {rl : list A | rl = rev l}. }
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v
index 6c514b16ee..1ecd9771eb 100644
--- a/test-suite/output/Extraction_matchs_2413.v
+++ b/test-suite/output/Extraction_matchs_2413.v
@@ -1,5 +1,7 @@
 (** Extraction : tests of optimizations of pattern matching *)
 
+Require Coq.extraction.Extraction.
+
 (** First, a few basic tests *)
 
 Definition test1 b :=
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index 3bf97c1312..f87f2e2a9d 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -1,4 +1,6 @@
 
+Require Import Coq.funind.FunInd.
+
 Definition iszero (n : nat) : bool :=
   match n with
   | O => true
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index d8f8042465..8419404925 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -147,6 +147,7 @@ Proof.
  intros; absurd (p < p); eauto with arith.
 Qed.
 
+Require Coq.extraction.Extraction.
 Extraction max.
 
 
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 0086e090bd..89be144152 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Coq.extraction.Extraction.
 Require Import Arith.
 Require Import List.
 
diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v
index 11bb25fda0..e770cf779a 100644
--- a/test-suite/success/extraction_dep.v
+++ b/test-suite/success/extraction_dep.v
@@ -1,6 +1,8 @@
 
 (** Examples of code elimination inside modules during extraction *)
 
+Require Coq.extraction.Extraction.
+
 (** NB: we should someday check the produced code instead of
     simply running the commands. *)
 
diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v
index dfdeff82ff..5bf807b1c6 100644
--- a/test-suite/success/extraction_impl.v
+++ b/test-suite/success/extraction_impl.v
@@ -4,6 +4,8 @@
 (** NB: we should someday check the produced code instead of
     simply running the commands. *)
 
+Require Coq.extraction.Extraction.
+
 (** Bug #4243, part 1 *)
 
 Inductive dnat : nat -> Type :=
diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v
index 7215bd9905..936d838c50 100644
--- a/test-suite/success/extraction_polyprop.v
+++ b/test-suite/success/extraction_polyprop.v
@@ -3,6 +3,8 @@
    code that segfaults. See Table.error_singleton_become_prop
    or S. Glondu's thesis for more details. *)
 
+Require Coq.extraction.Extraction.
+
 Definition f {X} (p : (nat -> X) * True) : X * nat :=
   (fst p 0, 0).
 
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 2fa7704941..789854b2d6 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -181,6 +181,8 @@ Record wrap (A : Type) := { unwrap : A; unwrap2 : A }.
 
 Definition term (x : wrap nat) := x.(unwrap).
 Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x.
+
+Require Coq.extraction.Extraction.
 Recursive Extraction term term'.
 (*Unset Printing Primitive Projection Parameters.*)
 
-- 
cgit v1.2.3


From 6c6c045a42dc591a0c35730e0abff80be0c8b9bb Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 14 Jun 2017 15:37:14 +0200
Subject: [typeclasses eauto] Fix bug #3943: non-termination in topological

sorting for the dependency order option.
---
 test-suite/bugs/closed/3943.v | 50 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 test-suite/bugs/closed/3943.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3943.v b/test-suite/bugs/closed/3943.v
new file mode 100644
index 0000000000..5e5ba816f9
--- /dev/null
+++ b/test-suite/bugs/closed/3943.v
@@ -0,0 +1,50 @@
+(* File reduced by coq-bug-finder from original input, then from 9492 lines to 119 lines *)
+(* coqc version 8.5beta1 (January 2015) compiled on Jan 18 2015 7:27:36 with OCaml 3.12.1
+   coqtop version 8.5beta1 (January 2015) *)
+
+Set Typeclasses Dependency Order.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Set Implicit Arguments.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+
+Record PreCategory := Build_PreCategory' {
+      object :> Type;
+      morphism : object -> object -> Type;
+      identity : forall x, morphism x x;
+      compose : forall s d d',
+                  morphism d d'
+                  -> morphism s d
+                  -> morphism s d' }.
+Arguments identity {!C%category} / x%object : rename.
+Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename.
+
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := {
+    morphism_inverse : morphism C d s;
+    left_inverse : compose morphism_inverse m = identity _;
+    right_inverse : compose m morphism_inverse = identity _ }.
+Arguments morphism_inverse {C s d} m {_}.
+Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope.
+
+Class Isomorphic {C : PreCategory} s d := {
+    morphism_isomorphic :> morphism C s d;
+    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
+Coercion morphism_isomorphic : Isomorphic >-> morphism.
+
+Variable C : PreCategory.
+Variables s d : C.
+
+Definition path_isomorphic (i j : Isomorphic s d)
+: @morphism_isomorphic _ _ _ i = @morphism_isomorphic _ _ _ j -> i = j.
+Admitted.
+
+Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q
+: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.
\ No newline at end of file
-- 
cgit v1.2.3


From 929dc481c91dc860b69b08dd65fb6f65d5650e23 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jun 2017 11:32:56 +0200
Subject: Remove dependency on -compat flag in coq_makefile test suite.

---
 test-suite/coq-makefile/arg/_CoqProject | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject
index afdb32e7cf..53dc963997 100644
--- a/test-suite/coq-makefile/arg/_CoqProject
+++ b/test-suite/coq-makefile/arg/_CoqProject
@@ -1,7 +1,7 @@
 -R theories test
 -R src test
 -I src
--arg "-compat 8.4"
+-arg "-w default"
 
 src/test_plugin.mlpack
 src/test.ml4
-- 
cgit v1.2.3


From db601b06b0880f573b6d1fa83de471679ce87ee7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 14 Jun 2017 18:18:37 +0200
Subject: plugins/ltac : avoid spurious .cmxs files

 In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs
 (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus :
  - wrong -for-pack used for their inner .cmx
  - dependency over modules not provided (for instance Tacenv, that ends
    up being a submodule of the pack ltac_plugin).
 But we were lucky, those files were actually never loaded, thanks to the
 several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin,
 and hence tell Coq that these modules are already known, preventing
 any attempt to load them.

 Anyway, this commit cleans up this mess (thanks PMP for the help)
---
 test-suite/bugs/closed/3612.v | 1 -
 test-suite/bugs/closed/3649.v | 2 --
 2 files changed, 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index 73709268a4..33e5d532ad 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -39,7 +39,6 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
 p = q.
 
 Declare ML Module "ltac_plugin".
-Declare ML Module "coretactics".
 
 Set Default Proof Mode "Classic".
 
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index 179f81e668..a664a1ef1d 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -3,7 +3,6 @@
 (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
 Declare ML Module "ltac_plugin".
-Declare ML Module "coretactics".
 Set Default Proof Mode "Classic".
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
@@ -14,7 +13,6 @@ Axiom admit : forall {T}, T.
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
 Reserved Infix "o" (at level 40, left associativity).
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
-Ltac constr_eq a b := let test := constr:(@idpath _ _ : a = b) in idtac.
 Global Set Primitive Projections.
 Delimit Scope morphism_scope with morphism.
 Record PreCategory :=
-- 
cgit v1.2.3


From 7b5fcef8a0fb3b97a3980f10596137234061990f Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 26 Apr 2017 15:24:35 +0200
Subject: Fix bugs

---
 test-suite/success/polymorphism.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 66ff55edcb..3e90825ab2 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -316,6 +316,26 @@ Module Hurkens'.
 
 Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
 
+Section test_letin_subtyping.
+  Universe i j k i' j' k'.
+  Constraint j < j'.
+
+  Context (W : Type) (X : box@{i j k} W).
+  Definition Y := X : box@{i' j' k'} W.
+
+  Universe i1 j1 k1 i2 j2 k2.
+  Constraint i1 < i2, k2 < k1.
+  Definition Z : box@{i1 j1 k1} W := {| unwrap := W |}.
+  Definition Z' : box@{i2 j2 k2} W := {| unwrap := W |}.
+  Lemma ZZ' : @eq (box@{i2 j2 k2} W) Z Z'.
+  Proof.
+    Set Printing All. Set Printing Universes.
+    cbv.
+    reflexivity.
+  Qed.
+
+End test_letin_subtyping.
+
 Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
 
 Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
-- 
cgit v1.2.3


From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 27 Apr 2017 20:16:35 +0200
Subject: Fix bugs and add an option for cumulativity

---
 test-suite/bugs/closed/3330.v     | 11 ++++++---
 test-suite/success/polymorphism.v | 52 ++++++++++++++++++++++++---------------
 2 files changed, 40 insertions(+), 23 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index e3b5e94356..a497e7a987 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -41,6 +41,8 @@ Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function
 
 Open Scope function_scope.
 
+Set Printing Universes. Set Printing All.
+
 Inductive paths {A : Type} (a : A) : A -> Type :=
   idpath : paths a a.
 
@@ -156,7 +158,8 @@ Delimit Scope morphism_scope with morphism.
 
 Delimit Scope category_scope with category.
 Delimit Scope object_scope with object.
-
+Set Printing Universes.
+Set Printing All.
 Record PreCategory :=
   Build_PreCategory' {
       object :> Type;
@@ -1069,8 +1072,10 @@ Section Adjunction.
   Variable F : Functor C D.
   Variable G : Functor D C.
 
-  Let Adjunction_Type := 
-    Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G).
+(*  Let Adjunction_Type := 
+    Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G).*)
+
+  Set Printing All. Set Printing Universes.
 
   Record AdjunctionHom :=
     {
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 3e90825ab2..f57cbcc2b7 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -316,26 +316,6 @@ Module Hurkens'.
 
 Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
 
-Section test_letin_subtyping.
-  Universe i j k i' j' k'.
-  Constraint j < j'.
-
-  Context (W : Type) (X : box@{i j k} W).
-  Definition Y := X : box@{i' j' k'} W.
-
-  Universe i1 j1 k1 i2 j2 k2.
-  Constraint i1 < i2, k2 < k1.
-  Definition Z : box@{i1 j1 k1} W := {| unwrap := W |}.
-  Definition Z' : box@{i2 j2 k2} W := {| unwrap := W |}.
-  Lemma ZZ' : @eq (box@{i2 j2 k2} W) Z Z'.
-  Proof.
-    Set Printing All. Set Printing Universes.
-    cbv.
-    reflexivity.
-  Qed.
-
-End test_letin_subtyping.
-
 Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
 
 Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
@@ -372,3 +352,35 @@ Module Anonymous.
   Check collapsethemiddle@{_ _}.
 
 End Anonymous.
+
+Module F.
+  Context {A B : Type}.
+  Definition foo : Type := B.
+End F.
+
+Set Universe Polymorphism.
+
+Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Section test_letin_subtyping.
+  Universe i j k i' j' k'.
+  Constraint j < j'.
+
+  Context (W : Type) (X : box@{i j k} W).
+  Definition Y := X : box@{i' j' k'} W.
+
+  Universe i1 j1 k1 i2 j2 k2.
+  Constraint i1 < i2.
+  Constraint k2 < k1.
+  Context (V : Type).
+
+  Definition Z : box@{i1 j1 k1} V := {| unwrap := V |}.
+  Definition Z' : box@{i2 j2 k2} V := {| unwrap := V |}.
+  Lemma ZZ' : @eq (box@{i2 j2 k2} V) Z Z'.
+  Proof.
+    Set Printing All. Set Printing Universes.
+    cbv.
+    reflexivity.
+  Qed.
+
+End test_letin_subtyping.
-- 
cgit v1.2.3


From 9903b47cdccc2fe98a905ab085cb24ca36de1aed Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 28 Apr 2017 11:12:26 +0200
Subject: Disable debug printing

Fix a mistake in record declaration
---
 test-suite/bugs/closed/3330.v     | 6 ++----
 test-suite/success/polymorphism.v | 2 +-
 2 files changed, 3 insertions(+), 5 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index a497e7a987..672fb3f131 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -1072,10 +1072,8 @@ Section Adjunction.
   Variable F : Functor C D.
   Variable G : Functor D C.
 
-(*  Let Adjunction_Type := 
-    Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G).*)
-
-  Set Printing All. Set Printing Universes.
+ Let Adjunction_Type := 
+    Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G).
 
   Record AdjunctionHom :=
     {
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index f57cbcc2b7..ecc988507c 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -360,7 +360,7 @@ End F.
 
 Set Universe Polymorphism.
 
-Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+Cumulative Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
 
 Section test_letin_subtyping.
   Universe i j k i' j' k'.
-- 
cgit v1.2.3


From d6898781f9cd52ac36a4891d7b169ddab7b8af50 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Tue, 2 May 2017 19:53:05 +0200
Subject: Correct coqchk reduction

---
 test-suite/coqchk/cumulativity.v | 52 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 test-suite/coqchk/cumulativity.v

(limited to 'test-suite')

diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
new file mode 100644
index 0000000000..5d245aaa5d
--- /dev/null
+++ b/test-suite/coqchk/cumulativity.v
@@ -0,0 +1,52 @@
+Set Universe Polymorphism.
+Set Ind Cumulativity.
+Set Printing Universes.
+
+Inductive List (A: Type) := nil | cons : A -> List A -> List A.
+
+Section ListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x.
+
+End ListLift.
+
+Lemma LiftL_Lem A (l : List A) : l = LiftL l.
+Proof. reflexivity. Qed.
+
+Section ListLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x.
+
+End ListLower.
+
+Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
+Proof. reflexivity. Qed.
+
+Inductive Tp := tp : Type -> Tp.
+
+Section TpLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x.
+
+End TpLift.
+
+Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
+Proof. reflexivity. Qed.
+
+Section TpLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x.
+
+End TpLower.
\ No newline at end of file
-- 
cgit v1.2.3


From 7b323421ba558011c304a686c4cd368e1ff39440 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 5 May 2017 13:33:18 +0200
Subject: Change the option to Set Inductive Cumulativity

This requires to change the status of Inductive (we have also changed
CoInductive and Variant) from keyword to identifier.
---
 test-suite/coqchk/cumulativity.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index 5d245aaa5d..3a8f9fa22f 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -1,5 +1,5 @@
 Set Universe Polymorphism.
-Set Ind Cumulativity.
+Set Inductive Cumulativity.
 Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
-- 
cgit v1.2.3


From 81a22cd3bee8fa6144d4eb46128ee8bb287ecb36 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 24 May 2017 14:40:36 +0200
Subject: Checker add test for non-trivial constraints

---
 test-suite/coqchk/cumulativity.v | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index 3a8f9fa22f..ecf9035bfe 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -49,4 +49,13 @@ Section TpLower.
 
   Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x.
 
-End TpLower.
\ No newline at end of file
+End TpLower.
+
+
+Section subtyping_test.
+  Universe i j.
+  Constraint i < j.
+
+  Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2.
+
+End subtyping_test.
\ No newline at end of file
-- 
cgit v1.2.3


From 3380f47d2bb38d549fcdac8fb073f9aa1f259a23 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Sat, 27 May 2017 09:48:53 +0200
Subject: Move (part of) tests from checker to success

Due to some unknown problem coqchk fails on some inductive types when it is
compiled with ocaml4.02.3+32bit and camlp5-4.16 which is the case for Travis
tests.
---
 test-suite/coqchk/cumulativity.v  | 43 +++++++++++++++------------
 test-suite/success/cumulativity.v | 61 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 86 insertions(+), 18 deletions(-)
 create mode 100644 test-suite/success/cumulativity.v

(limited to 'test-suite')

diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index ecf9035bfe..84121ea925 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -28,34 +28,41 @@ End ListLower.
 Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
 Proof. reflexivity. Qed.
 
-Inductive Tp := tp : Type -> Tp.
+(* I disable these tests because cqochk can't process them when compiled with
+   ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis!
 
-Section TpLift.
-  Universe i j.
+   I have added this file (including the commented parts below) in
+   test-suite/success/cumulativity.v which doesn't run coqchk on them.
+*)
 
-  Constraint i < j.
+(* Inductive Tp := tp : Type -> Tp. *)
 
-  Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x.
+(* Section TpLift. *)
+(*   Universe i j. *)
 
-End TpLift.
+(*   Constraint i < j. *)
 
-Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
-Proof. reflexivity. Qed.
+(*   Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. *)
 
-Section TpLower.
-  Universe i j.
+(* End TpLift. *)
 
-  Constraint i < j.
+(* Lemma LiftC_Lem (t : Tp) : LiftTp t = t. *)
+(* Proof. reflexivity. Qed. *)
 
-  Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x.
+(* Section TpLower. *)
+(*   Universe i j. *)
 
-End TpLower.
+(*   Constraint i < j. *)
 
+(*   Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. *)
 
-Section subtyping_test.
-  Universe i j.
-  Constraint i < j.
+(* End TpLower. *)
+
+
+(* Section subtyping_test. *)
+(*   Universe i j. *)
+(*   Constraint i < j. *)
 
-  Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2.
+(*   Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *)
 
-End subtyping_test.
\ No newline at end of file
+(* End subtyping_test. *)
\ No newline at end of file
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
new file mode 100644
index 0000000000..ecf9035bfe
--- /dev/null
+++ b/test-suite/success/cumulativity.v
@@ -0,0 +1,61 @@
+Set Universe Polymorphism.
+Set Inductive Cumulativity.
+Set Printing Universes.
+
+Inductive List (A: Type) := nil | cons : A -> List A -> List A.
+
+Section ListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x.
+
+End ListLift.
+
+Lemma LiftL_Lem A (l : List A) : l = LiftL l.
+Proof. reflexivity. Qed.
+
+Section ListLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x.
+
+End ListLower.
+
+Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
+Proof. reflexivity. Qed.
+
+Inductive Tp := tp : Type -> Tp.
+
+Section TpLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x.
+
+End TpLift.
+
+Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
+Proof. reflexivity. Qed.
+
+Section TpLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x.
+
+End TpLower.
+
+
+Section subtyping_test.
+  Universe i j.
+  Constraint i < j.
+
+  Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2.
+
+End subtyping_test.
\ No newline at end of file
-- 
cgit v1.2.3


From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 test-suite/coqchk/cumulativity.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index 84121ea925..a978f6b901 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -27,14 +27,13 @@ End ListLower.
 
 Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
 Proof. reflexivity. Qed.
-
-(* I disable these tests because cqochk can't process them when compiled with
+(*
+I disable these tests because cqochk can't process them when compiled with
    ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis!
 
    I have added this file (including the commented parts below) in
    test-suite/success/cumulativity.v which doesn't run coqchk on them.
 *)
-
 (* Inductive Tp := tp : Type -> Tp. *)
 
 (* Section TpLift. *)
-- 
cgit v1.2.3


From 15b1856edd593b39d63d23584a4f5acec0eeb592 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 15 Jun 2017 16:50:05 +0200
Subject: Fix a bug in cumulativity

---
 test-suite/success/cumulativity.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index ecf9035bfe..ebf817cfc5 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -58,4 +58,8 @@ Section subtyping_test.
 
   Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2.
 
-End subtyping_test.
\ No newline at end of file
+End subtyping_test.
+
+Record A : Type := { a :> Type; }.
+
+Record B (X : A) : Type := { b : X; }.
\ No newline at end of file
-- 
cgit v1.2.3


From f70f12b56e44abd9df4ad6941ee4941a761302fa Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 16 Jun 2017 11:07:23 +0200
Subject: Increase the time limit on 4366.v to make gitlab work better.

---
 test-suite/bugs/closed/4366.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v
index 6a5e9a4023..403c2d2026 100644
--- a/test-suite/bugs/closed/4366.v
+++ b/test-suite/bugs/closed/4366.v
@@ -10,6 +10,6 @@ end.
 Goal True.
 Proof.
 pose (v := stupid 24).
-Timeout 2 vm_compute in v.
+Timeout 4 vm_compute in v.
 exact I.
 Qed.
-- 
cgit v1.2.3


From d7e85f575fe6a41a700da9cd50236bef8ab03cf8 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 12 Jun 2017 17:50:18 +0200
Subject: romega: avoid potential slowdown when changing concl by reified
 version

 On some benchmarks provided by Chantal Keller a long time ago,
 romega was abnormally slow compared to omega (or lia).
 It turned out that the change of concl by reified version was
 triggering unnecessary unfolds of Z.add, instead of unfolding
 ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by
 the various Parameter Inline : no more indirections, Z_as_Int.plus
 is directly Z.add.

 Also use Tactics.convert_concl_no_check for this "change", as
 recommended by PMP.
---
 test-suite/success/ROmega3.v | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 test-suite/success/ROmega3.v

(limited to 'test-suite')

diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v
new file mode 100644
index 0000000000..fd4ff260b5
--- /dev/null
+++ b/test-suite/success/ROmega3.v
@@ -0,0 +1,31 @@
+
+Require Import ZArith ROmega.
+Local Open Scope Z_scope.
+
+(** Benchmark provided by Chantal Keller, that romega used to
+    solve far too slowly (compared to omega or lia). *)
+
+Parameter v4 : Z.
+Parameter v3 : Z.
+Parameter o4 : Z.
+Parameter s5 : Z.
+Parameter v2 : Z.
+Parameter o5 : Z.
+Parameter s6 : Z.
+Parameter v1 : Z.
+Parameter o6 : Z.
+Parameter s7 : Z.
+Parameter v0 : Z.
+Parameter o7 : Z.
+
+Lemma lemma_5833 :
+ ~ 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 +
+      (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
+         (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 8192
+\/
+  16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 +
+      (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
+         (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024.
+Proof.
+Timeout 1 romega. (* should take a few milliseconds, not seconds *)
+Timeout 1 Qed. (* ditto *)
-- 
cgit v1.2.3


From 396c77feb0cced3965f90f65c681e48c528636d5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 19 Jun 2017 17:40:48 +0200
Subject: Test case for bug 5578.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5578.v b/test-suite/bugs/closed/5578.v
new file mode 100644
index 0000000000..5bcdaa2f18
--- /dev/null
+++ b/test-suite/bugs/closed/5578.v
@@ -0,0 +1,57 @@
+(* File reduced by coq-bug-finder from original input, then from 1549 lines to  298 lines, then from 277 lines to 133 lines, then from 985 lines to 138 lines,  then from 206 lines to 139 lines, then from 203 lines to 142 lines, then from  262 lines to 152 lines, then from 567 lines to 151 lines, then from 3746 lines  to 151 lines, then from 577 lines to 151 lines, then from 187 lines to 151  lines, thenfrom 981 lines to 940 lines, then from 938 lines to 175 lines, then  from 589 lines to 205 lines, then from 3797 lines to 205 lines, then from 628  lines to 206 lines, then from 238 lines to 205 lines, then from 1346 lines to  213 lines, then from 633 lines to 214 lines, then from 243 lines to 213 lines,  then from 5656 lines to 245 lines, then from 661 lines to 272 lines, then from  3856 lines to 352 lines, then from 1266 lines to 407 lines, then from 421 lines  to 406 lines, then from 424 lines to 91 lines, then from 105 lines to 91 lines,  then from 85 lines to 55 lines, then from 69 lines to 55 lines *)
+(* coqc version trunk (May 2017) compiled on May 30 2017 13:28:59 with OCaml 
+4.02.3
+   coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-trunk,trunk  (fd36c0451c26e44b1b7e93299d3367ad2d35fee3) *)
+
+Class Proper {A} (R : A -> A -> Prop) (m : A) := mkp : R m m.
+Definition respectful {A B} (R : A -> A -> Prop) (R' : B -> B -> Prop) (f g : A  -> B) := forall x y, R x y -> R' (f x) (g y).
+Set Implicit Arguments.
+
+Class EqDec (A : Set) := {
+  eqb : A -> A -> bool ;
+  eqb_leibniz : forall x y, eqb x y = true <-> x = y
+}.
+
+Infix "?=" := eqb (at level 70) : eq_scope.
+
+Inductive Comp : Set -> Type :=
+| Bind : forall (A B : Set), Comp B -> (B -> Comp A) -> Comp A.
+
+Open Scope eq_scope.
+
+Goal forall (Rat : Set) (PositiveMap_t : Set -> Set)
+            type (t : type) (interp_type_list_message interp_type_rand  interp_type_message : nat -> Set),
+    (forall eta : nat, PositiveMap_t (interp_type_rand eta) ->  interp_type_list_message eta -> interp_type_message eta) ->
+    ((nat -> Rat) -> Prop) ->
+    forall (interp_type_sbool : nat -> Set) (interp_type0 : type -> nat -> Set),
+      (forall eta : nat,
+          (interp_type_list_message eta -> interp_type_message eta) ->  PositiveMap_t (interp_type_rand eta) -> interp_type0 t eta)
+      -> (forall (t0 : type) (eta : nat), EqDec (interp_type0 t0 eta))
+      -> (bool -> Comp bool) -> False.
+  clear.
+  intros Rat PositiveMap_t type t interp_type_list_message interp_type_rand  interp_type_message adv negligible interp_type_sbool
+         interp_type interp_term_fixed_t_x
+         EqDec_interp_type ret_bool.
+  assert (forall f adv' k
+                 (lem : forall (eta : nat) (evil_rands rands : PositiveMap_t 
+(interp_type_rand eta)),
+                     (interp_term_fixed_t_x eta (adv eta evil_rands) rands
+                                            ?= interp_term_fixed_t_x eta (adv  eta evil_rands) rands) = true),
+             (forall (eta : nat), Proper (respectful eq eq) (f eta))
+             -> negligible
+                  (fun eta : nat =>
+                     f eta (
+                         (Bind (k eta) (fun rands =>
+                          ret_bool (interp_term_fixed_t_x eta (adv' eta) rands  ?= interp_term_fixed_t_x eta (adv' eta) rands)))))).
+  Undo.
+  assert (forall f adv' k
+                 (lem : forall (eta : nat) (rands : PositiveMap_t 
+(interp_type_rand eta)),
+                     (interp_term_fixed_t_x eta (adv' eta) rands ?=  interp_term_fixed_t_x eta (adv' eta) rands) = true),
+             (forall (eta : nat), Proper (respectful eq eq) (f eta))
+             -> negligible
+                  (fun eta : nat =>
+                     f eta (
+                         (Bind (k eta) (fun rands =>
+                          ret_bool (interp_term_fixed_t_x eta (adv' eta) rands  ?= interp_term_fixed_t_x eta (adv' eta) rands)))))).
+ (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *)
\ No newline at end of file
-- 
cgit v1.2.3


From dbeb7210109f2e70e5fb55c65257ae2abd0bc3a0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Jun 2017 07:23:47 +0200
Subject: Should fix a false negative reported by deps-order.sh.

The files deps-order.sh and deps-checksum.sh were concurrently rm-ing
the files of the other.

Courtesy of Guillaume M.
---
 test-suite/misc/deps-checksum.sh | 2 +-
 test-suite/misc/deps-order.sh    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh
index 1e2afb7540..e07612b84c 100755
--- a/test-suite/misc/deps-checksum.sh
+++ b/test-suite/misc/deps-checksum.sh
@@ -1,4 +1,4 @@
-rm -f misc/deps/*/*.vo
+rm -f misc/deps/A/*.vo misc/deps/B/*.vo
 $coqc -R misc/deps/A A misc/deps/A/A.v
 $coqc -R misc/deps/B A misc/deps/B/A.v
 $coqc -R misc/deps/B A misc/deps/B/B.v
diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh
index 375b706f0a..00c5eb1bd5 100755
--- a/test-suite/misc/deps-order.sh
+++ b/test-suite/misc/deps-order.sh
@@ -1,7 +1,7 @@
 # Check that both coqdep and coqtop/coqc supports -R
 # Check that both coqdep and coqtop/coqc takes the later -R
 # See bugs 2242, 2337, 2339
-rm -f misc/deps/*/*.vo
+rm -f misc/deps/lib/*.vo misc/deps/client/*.vo
 tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
 $coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput
 diff -u misc/deps/deps.out $tmpoutput 2>&1
-- 
cgit v1.2.3


From d4a0e0bcc7689457340af5a3007a541b92e12301 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 22 Jun 2017 21:07:32 -0400
Subject: Add test-suite file for funind, extraction with compat 8.6

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

(limited to 'test-suite')

diff --git a/test-suite/success/FunindExtraction_compat86.v b/test-suite/success/FunindExtraction_compat86.v
new file mode 100644
index 0000000000..8912197d2f
--- /dev/null
+++ b/test-suite/success/FunindExtraction_compat86.v
@@ -0,0 +1,506 @@
+(* -*- coq-prog-args: ("-compat" "8.6") -*- *)
+
+Definition iszero (n : nat) : bool :=
+  match n with
+  | O => true
+  | _ => false
+  end.
+
+Functional Scheme iszero_ind := Induction for iszero Sort Prop.
+
+Lemma toto : forall n : nat, n = 0 -> iszero n = true.
+intros x eg.
+ functional induction iszero x; simpl.
+trivial.
+inversion eg.
+Qed.
+
+
+Function ftest (n m : nat) : nat :=
+  match n with
+  | O => match m with
+         | O => 0
+         | _ => 1
+         end
+  | S p => 0
+  end.
+(* MS: FIXME: apparently can't define R_ftest_complete. Rest of the file goes through. *)
+
+Lemma test1 : forall n m : nat, ftest n m <= 2.
+intros n m.
+ functional induction ftest n m; auto.
+Qed.
+
+Lemma test2 : forall m n, ~ 2 = ftest n m.
+Proof.
+intros n m;intro H.
+functional inversion H ftest.
+Qed.
+
+Lemma test3 : forall n m, ftest n m = 0 -> (n = 0 /\ m = 0)  \/ n <> 0.
+Proof.
+functional inversion 1 ftest;auto.
+Qed.
+
+
+Require Import Arith.
+Lemma test11 : forall m : nat, ftest 0 m <= 2.
+intros m.
+ functional induction ftest 0 m.
+auto.
+auto.
+auto with *.
+Qed.
+
+Function lamfix (m n : nat) {struct n } : nat :=
+  match n with
+    | O => m
+    | S p => lamfix m p
+  end.
+
+(* Parameter v1 v2 : nat. *)
+
+Lemma lamfix_lem : forall v1 v2 : nat, lamfix v1 v2 = v1.
+intros v1 v2.
+ functional induction lamfix v1 v2.
+trivial.
+assumption.
+Defined.
+
+
+
+(* polymorphic function *)
+Require Import List.
+
+Functional Scheme app_ind := Induction for app Sort Prop.
+
+Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'.
+intros A l l'.
+ functional induction app A l l';  intuition.
+ rewrite <- H0; trivial.
+Qed.
+
+
+
+
+
+Require Export Arith.
+
+
+Function trivfun (n : nat) : nat :=
+  match n with
+  | O => 0
+  | S m => trivfun m
+  end.
+
+
+(* essaie de parametre variables non locaux:*)
+
+Parameter varessai : nat.
+
+Lemma first_try : trivfun varessai = 0.
+ functional induction trivfun varessai.
+trivial.
+assumption.
+Defined.
+
+
+ Functional Scheme triv_ind := Induction for trivfun Sort Prop.
+
+Lemma bisrepetita : forall n' : nat, trivfun n' = 0.
+intros n'.
+ functional induction trivfun n'.
+trivial.
+assumption.
+Qed.
+
+
+
+
+
+
+
+Function iseven (n : nat) : bool :=
+  match n with
+  | O => true
+  | S (S m) => iseven m
+  | _ => false
+  end.
+
+
+Function funex (n : nat) : nat :=
+  match iseven n with
+  | true => n
+  | false => match n with
+             | O => 0
+             | S r => funex r
+             end
+  end.
+
+
+Function nat_equal_bool (n m : nat) {struct n} : bool :=
+  match n with
+  | O => match m with
+         | O => true
+         | _ => false
+         end
+  | S p => match m with
+           | O => false
+           | S q => nat_equal_bool p q
+           end
+  end.
+
+
+Require Export Div2.
+Require Import Nat.
+Functional Scheme div2_ind := Induction for div2 Sort Prop.
+Lemma div2_inf : forall n : nat, div2 n <= n.
+intros n.
+ functional induction div2 n.
+auto.
+auto.
+
+apply le_S.
+apply le_n_S.
+exact IHn0.
+Qed.
+
+(* reuse this lemma as a scheme:*)
+
+Function nested_lam (n : nat) : nat -> nat :=
+  match n with
+  | O => fun m : nat => 0
+  | S n' => fun m : nat => m + nested_lam n' m
+  end.
+
+
+Lemma nest : forall n m : nat, nested_lam n m = n * m.
+intros n m.
+ functional induction nested_lam n m; simpl;auto.
+Qed.
+
+
+Function essai (x : nat) (p : nat * nat) {struct x} : nat :=
+  let (n, m) := (p: nat*nat) in
+  match n with
+  | O => 0
+  | S q => match x with
+           | O => 1
+           | S r => S (essai r (q, m))
+           end
+  end.
+
+Lemma essai_essai :
+ forall (x : nat) (p : nat * nat), let (n, m) := p in 0 < n -> 0 < essai x p.
+intros x p.
+ functional induction essai x p; intros.
+inversion H.
+auto with arith.
+ auto with arith.
+Qed.
+
+Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
+  let x := nat_equal_bool m 5 in
+  let y := 0 in
+  match n with
+  | O => y
+  | S q =>
+      let recapp := plus_x_not_five'' q m in
+      match x with
+      | true => S recapp
+      | false => S recapp
+      end
+  end.
+
+Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x.
+intros a b.
+ functional induction plus_x_not_five'' a b; intros hyp; simpl; auto.
+Qed.
+
+Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
+intros n m.
+ functional induction nat_equal_bool n m; simpl; intros hyp; auto.
+rewrite <- hyp in y; simpl in y;tauto.
+inversion hyp.
+Qed.
+
+Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m.
+intros n m.
+ functional induction nat_equal_bool n m; simpl; intros eg; auto.
+inversion eg.
+inversion eg.
+Qed.
+
+
+Inductive istrue : bool -> Prop :=
+    istrue0 : istrue true.
+
+Functional Scheme add_ind := Induction for add Sort Prop.
+
+Lemma inf_x_plusxy' : forall x y : nat, x <= x + y.
+intros n m.
+ functional induction add n m; intros.
+auto with arith.
+auto with arith.
+Qed.
+
+
+Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0.
+intros n.
+unfold plus.
+ functional induction plus n 0; intros.
+auto with arith.
+apply le_n_S.
+assumption.
+Qed.
+
+Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x.
+intros n.
+ functional induction plus 0 n; intros; auto with arith.
+Qed.
+
+Function mod2 (n : nat) : nat :=
+  match n with
+  | O => 0
+  | S (S m) => S (mod2 m)
+  | _ => 0
+  end.
+
+Lemma princ_mod2 : forall n : nat, mod2 n <= n.
+intros n.
+ functional induction mod2 n; simpl; auto with arith.
+Qed.
+
+Function isfour (n : nat) : bool :=
+  match n with
+  | S (S (S (S O))) => true
+  | _ => false
+  end.
+
+Function isononeorfour (n : nat) : bool :=
+  match n with
+  | S O => true
+  | S (S (S (S O))) => true
+  | _ => false
+  end.
+
+Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n).
+intros n.
+ functional induction isononeorfour n; intros istr; simpl;
+ inversion istr.
+apply istrue0.
+destruct n. inversion istr.
+destruct n. tauto.
+destruct n. inversion istr.
+destruct n. inversion istr.
+destruct n. tauto.
+simpl in *. inversion H0.
+Qed.
+
+Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n).
+intros n.
+ functional induction isononeorfour n; intros m istr; inversion istr.
+apply istrue0.
+rewrite H in y; simpl in y;tauto.
+Qed.
+
+Function ftest4 (n m : nat) : nat :=
+  match n with
+  | O => match m with
+         | O => 0
+         | S q => 1
+         end
+  | S p => match m with
+           | O => 0
+           | S r => 1
+           end
+  end.
+
+Lemma test4 : forall n m : nat, ftest n m <= 2.
+intros n m.
+ functional induction ftest n m; auto with arith.
+Qed.
+
+Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2.
+intros n m.
+assert ({n0 | n0 = S n}).
+exists (S n);reflexivity.
+destruct H as [n0 H1].
+rewrite <- H1;revert H1.
+ functional induction ftest4 n0 m.
+inversion 1.
+inversion 1.
+
+auto with arith.
+auto with arith.
+Qed.
+
+Function ftest44 (x : nat * nat) (n m : nat) : nat :=
+  let (p, q) := (x: nat*nat) in
+  match n with
+  | O => match m with
+         | O => 0
+         | S q => 1
+         end
+  | S p => match m with
+           | O => 0
+           | S r => 1
+           end
+  end.
+
+Lemma test44 :
+ forall (pq : nat * nat) (n m o r s : nat), ftest44 pq n (S m) <= 2.
+intros pq n m o r s.
+ functional induction ftest44 pq n (S m).
+auto with arith.
+auto with arith.
+auto with arith.
+auto with arith.
+Qed.
+
+Function ftest2 (n m : nat) {struct n} : nat :=
+  match n with
+  | O => match m with
+         | O => 0
+         | S q => 0
+         end
+  | S p => ftest2 p m
+  end.
+
+Lemma test2' : forall n m : nat, ftest2 n m <= 2.
+intros n m.
+ functional induction ftest2 n m; simpl; intros; auto.
+Qed.
+
+Function ftest3 (n m : nat) {struct n} : nat :=
+  match n with
+  | O => 0
+  | S p => match m with
+           | O => ftest3 p 0
+           | S r => 0
+           end
+  end.
+
+Lemma test3' : forall n m : nat, ftest3 n m <= 2.
+intros n m.
+ functional induction ftest3 n m.
+intros.
+auto.
+intros.
+auto.
+intros.
+simpl.
+auto.
+Qed.
+
+Function ftest5 (n m : nat) {struct n} : nat :=
+  match n with
+  | O => 0
+  | S p => match m with
+           | O => ftest5 p 0
+           | S r => ftest5 p r
+           end
+  end.
+
+Lemma test5 : forall n m : nat, ftest5 n m <= 2.
+intros n m.
+ functional induction ftest5 n m.
+intros.
+auto.
+intros.
+auto.
+intros.
+simpl.
+auto.
+Qed.
+
+Function ftest7 (n : nat) : nat :=
+  match ftest5 n 0 with
+  | O => 0
+  | S r => 0
+  end.
+
+Lemma essai7 :
+ forall (Hrec : forall n : nat, ftest5 n 0 = 0 -> ftest7 n <= 2)
+   (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2)
+   (n : nat), ftest7 n <= 2.
+intros hyp1 hyp2 n.
+ functional induction ftest7 n; auto.
+Qed.
+
+Function ftest6 (n m : nat) {struct n} : nat :=
+  match n with
+  | O => 0
+  | S p => match ftest5 p 0 with
+           | O => ftest6 p 0
+           | S r => ftest6 p r
+           end
+  end.
+
+
+Lemma princ6 :
+ (forall n m : nat, n = 0 -> ftest6 0 m <= 2) ->
+ (forall n m p : nat,
+  ftest6 p 0 <= 2 -> ftest5 p 0 = 0 -> n = S p -> ftest6 (S p) m <= 2) ->
+ (forall n m p r : nat,
+  ftest6 p r <= 2 -> ftest5 p 0 = S r -> n = S p -> ftest6 (S p) m <= 2) ->
+ forall x y : nat, ftest6 x y <= 2.
+intros hyp1 hyp2 hyp3 n m.
+generalize hyp1 hyp2 hyp3.
+clear hyp1 hyp2 hyp3.
+ functional induction ftest6 n m; auto.
+Qed.
+
+Lemma essai6 : forall n m : nat, ftest6 n m <= 2.
+intros n m.
+ functional induction ftest6 n m; simpl; auto.
+Qed.
+
+(* Some tests with modules *)
+Module M.
+Function test_m (n:nat) : nat :=
+  match n with
+    | 0 => 0
+    | S n =>  S (S (test_m n))
+  end.
+
+Lemma test_m_is_double :  forall n, div2 (test_m n) = n.
+Proof.
+intros n.
+functional induction (test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.
+End M.
+(* We redefine a new Function with the same name *)
+Function test_m (n:nat) : nat :=
+  pred n.
+
+Lemma test_m_is_pred : forall n, test_m n = pred n.
+Proof.
+intro n.
+functional induction (test_m n). (* the test_m_ind to use is the last defined  saying that test_m = pred*)
+reflexivity.
+Qed.
+
+(* Checks if the dot notation are correctly treated in infos *)
+Lemma M_test_m_is_double : forall n, div2 (M.test_m n) = n.
+intro n.
+(* here we should apply M.test_m_ind *)
+functional induction (M.test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.
+
+Import M.
+(* Now test_m is the one which defines double *)
+
+Lemma test_m_is_double : forall n, div2 (M.test_m n) = n.
+intro n.
+(* here we should apply M.test_m_ind *)
+functional induction (test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.
+
+Extraction iszero.
-- 
cgit v1.2.3


From 181cb78d09ba55c7a6d62b333b26595a4fbb360a Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Fri, 23 Jun 2017 15:06:49 +0200
Subject: closing bug #4250

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4250.v b/test-suite/bugs/closed/4250.v
new file mode 100644
index 0000000000..74cacf559a
--- /dev/null
+++ b/test-suite/bugs/closed/4250.v
@@ -0,0 +1,11 @@
+Require Import FunInd.
+Require  Vector.
+Generalizable All Variables.
+
+Definition f `{n:nat , u:Vector.t A n} := n.
+
+Function f2 {A:Type} {n:nat} {v:Vector.t A n} : nat := n.
+
+(* fails with "The reference A was not found in the current environment." *)
+Function f3 `{n:nat , u:Vector.t A n} := u.
+Check R_f3_complete.
\ No newline at end of file
-- 
cgit v1.2.3


From 10c81e90a836c8abea32bc6157976b9adf7775fa Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Thu, 29 Jun 2017 17:27:04 +0200
Subject: closing bug #5618 introduce by PR 828

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5618.v b/test-suite/bugs/closed/5618.v
new file mode 100644
index 0000000000..ab88a88f44
--- /dev/null
+++ b/test-suite/bugs/closed/5618.v
@@ -0,0 +1,9 @@
+Require Import FunInd.
+
+Function test {T} (v : T) (x : nat) : nat :=
+  match x with
+  | 0 => 0
+  | S x' => test v x'
+  end.
+
+Check R_test_complete.
\ No newline at end of file
-- 
cgit v1.2.3