From fd47b2d2638518fe62ce9c63557d2dab219d9558 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Thu, 30 Jun 2016 19:41:53 +0200
Subject: Goal selectors now use the keyword [only].

This fixes some parsing problems when doing things like
[let n := 2 in idtac n]. See bug #4877.
---
 test-suite/bugs/closed/4877.v      | 12 ++++++++++++
 test-suite/success/goal_selector.v |  8 ++++----
 2 files changed, 16 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/4877.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4877.v b/test-suite/bugs/closed/4877.v
new file mode 100644
index 0000000000..7e3c78dc2e
--- /dev/null
+++ b/test-suite/bugs/closed/4877.v
@@ -0,0 +1,12 @@
+Ltac induction_last :=
+  let v := match goal with
+           | |- forall x y, _ = _ -> _ => 1
+           | |- forall x y, _ -> _ = _ -> _ => 2
+           | |- forall x y, _ -> _ -> _ = _ -> _ => 3
+           end in
+  induction v.
+
+Goal forall n m : nat, True -> n = m -> m = n.
+  induction_last.
+  reflexivity.
+Qed.
\ No newline at end of file
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
index 91fb54d9a1..8681405175 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -34,7 +34,7 @@ Qed.
 
 Goal True -> True.
 Proof.
-  intros y; 1-2 : repeat idtac.
+  intros y; only 1-2 : repeat idtac.
   1-1:match goal with y : _ |- _ => let x := y in idtac x end.
   Fail 1-1:let x := y in idtac x.
   1:let x := y in idtac x.
@@ -44,12 +44,12 @@ Qed.
 Goal True /\ (True /\ True).
 Proof.
   dup.
-  - split; 2: (split; exact I).
+  - split; only 2: (split; exact I).
     exact I.
-  - split; 2: split; exact I.
+  - split; only 2: split; exact I.
 Qed.
 
 Goal True -> exists (x : Prop), x.
 Proof.
-  intro H; eexists ?[x]. [x]: exact True. 1: assumption.
+  intro H; eexists ?[x]; only [x]: exact True. 1: assumption.
 Qed.
-- 
cgit v1.2.3


From 751fa3aa8aed28946b45d8932514913c86ce8f5a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 27 Sep 2016 15:26:37 +0200
Subject: Add fixed test-suite file for bug #4527

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
new file mode 100644
index 0000000000..4ca6fe78cd
--- /dev/null
+++ b/test-suite/bugs/closed/4527.v
@@ -0,0 +1,267 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 1199 lines to 
+430 lines, then from 444 lines to 430 lines, then from 964 lines to 255 lines, 
+then from 269 lines to 255 lines *)
+(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
+4.01.0
+   coqtop version 8.5 (January 2016) *)
+Inductive False := .
+Axiom proof_admitted : False.
+Tactic Notation "admit" := case proof_admitted.
+Require Coq.Init.Datatypes.
+
+Import Coq.Init.Notations.
+
+Global Set Universe Polymorphism.
+
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+
+Inductive True : Type :=
+  I : True.
+Module Export Datatypes.
+
+Set Implicit Arguments.
+Notation nat := Coq.Init.Datatypes.nat.
+Notation S := Coq.Init.Datatypes.S.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+
+Notation "x * y" := (prod x y) : type_scope.
+
+Open Scope nat_scope.
+
+End Datatypes.
+Module Export Specif.
+
+Set Implicit Arguments.
+
+Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P 
+proj1_sig }.
+
+Notation sigT := sig (only parsing).
+
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+
+Notation projT1 := proj1_sig (only parsing).
+Notation projT2 := proj2_sig (only parsing).
+
+End Specif.
+Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+
+Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in 
+Type@{i}.
+
+Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in
+                                        let ge := ((fun x => x) : Type1@{j} -> 
+Type@{i}) in Type@{i}.
+
+Notation idmap := (fun x => x).
+Delimit Scope function_scope with function.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope fibration_scope.
+Open Scope function_scope.
+
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g%function f%function) (at level 40, left 
+associativity) : function_scope.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_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.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : 
+type_scope.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+
+Arguments eisretr {A B}%type_scope f%function_scope {_} _.
+Arguments eissect {A B}%type_scope f%function_scope {_} _.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : 
+function_scope.
+
+Inductive Unit : Type1 :=
+    tt : Unit.
+
+Local Open Scope path_scope.
+
+Section EquivInverse.
+
+  Context {A B : Type} (f : A -> B) {feq : IsEquiv f}.
+
+  Theorem other_adj (b : B) : eissect f (f^-1 b) = ap f^-1 (eisretr f b).
+admit.
+Defined.
+
+  Global Instance isequiv_inverse : IsEquiv f^-1 | 10000
+    := BuildIsEquiv B A f^-1 f (eissect f) (eisretr f) other_adj.
+End EquivInverse.
+
+Section Adjointify.
+
+  Context {A B : Type} (f : A -> B) (g : B -> A).
+  Context (isretr : Sect g f) (issect : Sect f g).
+
+  Let issect' := fun x =>
+    ap g (ap f (issect x)^)  @  ap g (isretr (f x))  @  issect x.
+
+  Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a).
+admit.
+Defined.
+
+  Definition isequiv_adjointify : IsEquiv f
+    := BuildIsEquiv A B f g isretr issect' is_adjoint'.
+
+End Adjointify.
+
+  Definition ExtensionAlong {A B : Type} (f : A -> B)
+             (P : B -> Type) (d : forall x:A, P (f x))
+    := { s : forall y:B, P y & forall x:A, s (f x) = d x }.
+
+  Fixpoint ExtendableAlong@{i j k l}
+           (n : nat) {A : Type@{i}} {B : Type@{j}}
+           (f : A -> B) (C : B -> Type@{k}) : Type@{l}
+    := match n with
+         | 0 => Unit@{l}
+         | S n => (forall (g : forall a, C (f a)),
+                     ExtensionAlong@{i j k l l} f C g) *
+                  forall (h k : forall b, C b),
+                    ExtendableAlong n f (fun b => h b = k b)
+       end.
+
+  Definition ooExtendableAlong@{i j k l}
+             {A : Type@{i}} {B : Type@{j}}
+             (f : A -> B) (C : B -> Type@{k}) : Type@{l}
+    := forall n, ExtendableAlong@{i j k l} n f C.
+
+Module Type ReflectiveSubuniverses.
+
+  Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}.
+
+  Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
+                            Type2le@{i a} -> Type2le@{i a}.
+
+  Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
+                   Type2le@{i a} -> Type2le@{i a}.
+
+  Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : 
+Type@{i}),
+                               In@{u a i} O (O_reflector@{u a i} O T).
+
+  Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : 
+Type@{i}),
+                   T -> O_reflector@{u a i} O T.
+
+  Parameter inO_equiv_inO@{u a i j k} :
+      forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j})
+             (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f),
+
+        let gei := ((fun x => x) : Type@{i} -> Type@{k}) in
+        let gej := ((fun x => x) : Type@{j} -> Type@{k}) in
+        In@{u a j} O U.
+
+  Parameter extendable_to_O@{u a i j k}
+  : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : 
+Type2le@{j a}} {Q_inO : In@{u a j} O Q},
+      ooExtendableAlong@{i i j k} (to O P) (fun _ => Q).
+
+End ReflectiveSubuniverses.
+
+Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses).
+Export Os.
+
+Existing Class In.
+
+  Coercion O_reflector : ReflectiveSubuniverse >-> Funclass.
+
+Arguments inO_equiv_inO {O} T {U} {_} f {_}.
+Global Existing Instance O_inO.
+
+Section ORecursion.
+  Context {O : ReflectiveSubuniverse}.
+
+  Definition O_indpaths {P Q : Type} {Q_inO : In O Q}
+             (g h : O P -> Q) (p : g o to O P == h o to O P)
+  : g == h
+  := (fst (snd (extendable_to_O O 2) g h) p).1.
+
+  Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q}
+             (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P)
+  : O_indpaths g h p (to O P x) = p x
+  := (fst (snd (extendable_to_O O 2) g h) p).2 x.
+
+End ORecursion.
+
+Section Reflective_Subuniverse.
+  Universes Ou Oa.
+  Context (O : ReflectiveSubuniverse@{Ou Oa}).
+
+    Definition inO_isequiv_to_O (T:Type)
+    : IsEquiv (to O T) -> In O T
+    := fun _ => inO_equiv_inO (O T) (to O T)^-1.
+
+    Definition inO_to_O_retract (T:Type) (mu : O T -> T)
+    : Sect (to O T) mu -> In O T.
+    Proof.
+      unfold Sect; intros H.
+      apply inO_isequiv_to_O.
+      apply isequiv_adjointify with (g:=mu).
+      -
+ refine (O_indpaths (to O T o mu) idmap _).
+        intros x; exact (ap (to O T) (H x)).
+      -
+ exact H.
+    Defined.
+
+    Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : 
+S)    : In@{Ou Oa i} O (x=y).
+    Proof.
+      simple refine (inO_to_O_retract@{i j} _ _ _); intro u.
+      -
+ assert (p : (fun _ : O (x=y) => x) == (fun _=> y)).
+        {
+ refine (O_indpaths _ _ _); simpl.
+          intro v; exact v.
+}
+        exact (p u).
+      -
+ hnf.
+        rewrite O_indpaths_beta; reflexivity.
+    Qed.
+    Check inO_paths@{Type Type}.
-- 
cgit v1.2.3


From 8e0f29cb69f06b64d74b18b09fb6a717034f1140 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 22 Aug 2016 08:32:59 +0200
Subject: Typeclass backtracking example by J. Leivant

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

(limited to 'test-suite')

diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 590f6e191f..bb1cf06541 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -46,6 +46,25 @@ Module Backtracking.
   Qed.
   
   Unset Typeclasses Debug.
+
+  Module Leivant.
+    Axiom A : Type.
+    Existing Class A.
+    Axioms a b c d e: A.
+    
+    Ltac get_value H := eval cbv delta [H] in H.
+    
+    Goal True.
+      Fail refine (let H := _ : A in _); let v := get_value H in idtac v; fail.
+    Admitted.
+
+    Goal exists x:A, x=a.
+      unshelve evar (t : A). all:cycle 1.
+      refine (@ex_intro _ _ t _).
+      all:cycle 1.
+      all:(typeclasses eauto + reflexivity).
+    Qed.      
+  End Leivant.
 End Backtracking.
 
 
-- 
cgit v1.2.3


From 875f235dd0413faa34f7d46afc25d2eb90e386e5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Sep 2016 17:01:26 +0200
Subject: Fix bug #4723 and FIXME in API for solve_by_tac

This avoids leakage of universes. Also makes
Program Lemma/Fact work again, it tries to solve the
remaining evars using the obligation tactic.
---
 test-suite/bugs/closed/4723.v | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 test-suite/bugs/closed/4723.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v
new file mode 100644
index 0000000000..8884812102
--- /dev/null
+++ b/test-suite/bugs/closed/4723.v
@@ -0,0 +1,28 @@
+
+Require Coq.Program.Tactics.
+
+Record Matrix (m n : nat).
+
+Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q):
+  Matrix (m*p) (n*q). Admitted.
+
+Fail Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+
+Ltac Obligation Tactic := admit.
+Fail Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+
+Axiom cheat : forall {A}, A.
+Obligation Tactic := apply cheat.
+
+Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+admit.
+Admitted.
\ No newline at end of file
-- 
cgit v1.2.3


From a6832ccfacd9c105b23a9a77dadc3202f7af26fc Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 29 Sep 2016 10:46:53 +0200
Subject: Argument : assert does fail if no arg is given (fix #4864)

---
 test-suite/output/Arguments.v     | 2 +-
 test-suite/success/simpl_tuning.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 05eeaac631..bd9240476f 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -17,7 +17,7 @@ Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
 Arguments fcomp {_ _ _}%type_scope f g x /.
 About fcomp.
 Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
 About volatile.
 Set Implicit Arguments.
 Section S1.
diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v
index d4191b939b..2728672f30 100644
--- a/test-suite/success/simpl_tuning.v
+++ b/test-suite/success/simpl_tuning.v
@@ -106,7 +106,7 @@ match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end.
 Abort. 
 
 Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
 
 Lemma foo : volatile = volatile.
 simpl.
-- 
cgit v1.2.3


From 5348a615a484e379896deac8a6944af1f92b2d4c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Sep 2016 17:58:06 +0200
Subject: test-suite: fix sed on OS X, does not handle +

---
 test-suite/Makefile | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 1dfbb29ff0..a40ea80ae4 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -304,16 +304,16 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
 	    | grep -v "^<W>" \
-	    | sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \
+	    | sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \
 	          -e 's/\s*0\.\s*//g' \
 		  -e 's/\s*[-+]nan\s*//g' \
 		  -e 's/\s*[-+]inf\s*//g' \
 	    > $$tmpoutput; \
-	  sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \
+	  sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \
 		-e 's/\s*0\.\s*//g' \
 		-e 's/\s*[-+]nan\s*//g' \
 		-e 's/\s*[-+]inf\s*//g' \
-       	       $*.out > $$tmpexpected; \
+	       $*.out > $$tmpexpected; \
 	  diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
-- 
cgit v1.2.3


From 4e3d4646788c96f16193df14a81aa79938812194 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 29 Sep 2016 09:35:07 +0200
Subject: Fix a bug in subst releaved by an OCaml warning.

---
 test-suite/output/subst.out | 208 ++++++++++++++++++++++++++++++++++++++++++++
 test-suite/output/subst.v   |  11 +++
 2 files changed, 219 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
index 209b2bc26f..dbb9e09a43 100644
--- a/test-suite/output/subst.out
+++ b/test-suite/output/subst.out
@@ -26,6 +26,19 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
   x, y : nat
   Hx : x = 0
   Hy : y = 0
@@ -39,6 +52,45 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
   H1 : 0 = 1
   HA : True
   H2 : 0 = 2
@@ -49,6 +101,58 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
   y, z : nat
   Hy : y = 0
   Hz : z = 0
@@ -75,6 +179,19 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
   x, y : nat
   Hx : x = 0
   Hy : y = 0
@@ -88,6 +205,45 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  HB : True
+  H4 : z = 4
+  H3 : 0 = 3
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
   HA, HB : True
   H4 : 0 = 4
   H3 : 0 = 3
@@ -95,3 +251,55 @@
   H2 : 0 = 2
   ============================
   True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  HB : True
+  H4 : z = 4
+  H3 : 0 = 3
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v
index e48aa6bb28..91bdd03e02 100644
--- a/test-suite/output/subst.v
+++ b/test-suite/output/subst.v
@@ -45,4 +45,15 @@ Show.
 trivial.
 Qed.
 
+(* A bug revealed by OCaml 4.03 warnings *)
+Goal forall y, let x:=0 in y=x -> y=y.
+intros * H;
+subst.
+Fail clear H. (* Was working *)
+Abort.
 
+Goal forall y, let x:=0 in y=x -> y=y.
+intros * H;
+subst.
+Fail clear H. (* Was failing before fix *)
+Abort.
-- 
cgit v1.2.3


From c1c488d08857636381d6cbf3a9202e7123923dd0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 29 Sep 2016 15:17:02 +0200
Subject: Fix bug #5011: Anomaly on [Existing Class].

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5011.v b/test-suite/bugs/closed/5011.v
new file mode 100644
index 0000000000..c3043ca5d1
--- /dev/null
+++ b/test-suite/bugs/closed/5011.v
@@ -0,0 +1,2 @@
+Record decoder (n : nat) W := { decode : W -> nat }.
+Existing Class decoder.
-- 
cgit v1.2.3


From 9615c025a2a09b69f2001d44a66a1fddef74e680 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Sep 2016 15:51:18 +0200
Subject: Fix bug #4869, allow Prop, Set, and level names in constraints.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v
new file mode 100644
index 0000000000..6d21b66fe9
--- /dev/null
+++ b/test-suite/bugs/closed/4869.v
@@ -0,0 +1,18 @@
+Universes i.
+
+Fail Constraint i < Set.
+Fail Constraint i <= Set.
+Fail Constraint i = Set.
+Constraint Set <= i.
+Constraint Set < i.
+Fail Constraint i < j. (* undeclared j *)
+Fail Constraint i < Type. (* anonymous *)
+
+Set Universe Polymorphism.
+
+Section Foo.
+  Universe j.
+  Constraint Set < j.
+
+  Definition foo := Type@{j}.
+End Foo.
\ No newline at end of file
-- 
cgit v1.2.3


From cf87e73ff4dd0b9c70436d66d326ae839868ba78 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Sep 2016 17:26:14 +0200
Subject: Fix bug #5036 autorewrite, sections and universes

Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
---
 test-suite/bugs/closed/5036.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/5036.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v
new file mode 100644
index 0000000000..12c958be67
--- /dev/null
+++ b/test-suite/bugs/closed/5036.v
@@ -0,0 +1,10 @@
+Section foo.
+  Context (F : Type -> Type).
+  Context (admit : forall {T}, F T = True).
+  Hint Rewrite (fun T => @admit T).
+  Lemma bad : F False.
+  Proof.
+    autorewrite with core.
+    constructor.
+  Qed.
+End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
\ No newline at end of file
-- 
cgit v1.2.3


From 601fd9343a241706c0a205aaf8e08255753c3780 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 29 Sep 2016 15:23:07 +0200
Subject: Arguments: cleanup + detect discrepancy rename/implicit (#3753)

It seems warnings are not taken into account in output/
tests.
---
 test-suite/bugs/closed/3045.v            |  2 +-
 test-suite/bugs/closed/3753.v            |  4 ++++
 test-suite/bugs/opened/3753.v            |  4 ----
 test-suite/output/Arguments_renaming.out | 20 +++++++++++++++++---
 test-suite/output/Arguments_renaming.v   |  2 +-
 5 files changed, 23 insertions(+), 9 deletions(-)
 create mode 100644 test-suite/bugs/closed/3753.v
 delete mode 100644 test-suite/bugs/opened/3753.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3045.v b/test-suite/bugs/closed/3045.v
index ef110ad0d0..5f80013df2 100644
--- a/test-suite/bugs/closed/3045.v
+++ b/test-suite/bugs/closed/3045.v
@@ -12,7 +12,7 @@ Record SpecializedCategory (obj : Type) :=
     Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
   }.
 
-Arguments Compose {obj} [C s d d'] m1 m2 : rename.
+Arguments Compose {obj} [C s d d'] _ _ : rename.
 
 Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
 | ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'.
diff --git a/test-suite/bugs/closed/3753.v b/test-suite/bugs/closed/3753.v
new file mode 100644
index 0000000000..5bfbee9494
--- /dev/null
+++ b/test-suite/bugs/closed/3753.v
@@ -0,0 +1,4 @@
+Axiom foo : Type -> Type.
+Axiom bar : forall (T : Type), T -> foo T.
+Arguments bar A x : rename.
+About bar.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3753.v b/test-suite/bugs/opened/3753.v
deleted file mode 100644
index 05d77c831b..0000000000
--- a/test-suite/bugs/opened/3753.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Axiom foo : Type -> Type.
-Axiom bar : forall (T : Type), T -> foo T.
-Arguments bar A x : rename.
-Fail About bar.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 3488cb3056..815305581c 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,9 +1,20 @@
+File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 1, characters 0-36:
+Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
+[arguments-assert,vernacular]
 The command has indeed failed with message:
 Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
-The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
-Argument A renamed to T.
+File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25:
+Warning: Ignoring rename of A into T. Only implicit arguments can be renamed.
+[arguments-assert,vernacular]
+File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25:
+Warning: This command is just asserting the number and names of arguments of
+identity. If this is what you want add ': assert' to silence the warning. If
+you want to clear implicit arguments add ': clear implicits'. If you want to
+clear notation scopes add ': clear scopes' [arguments-assert,vernacular]
+File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 4, characters 0-40:
+Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
+[arguments-assert,vernacular]
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
@@ -110,6 +121,9 @@ The command has indeed failed with message:
 Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
 Error: Extra argument y.
+File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 53, characters 0-26:
+Warning: Ignoring rename of x into s. Only implicit arguments can be renamed.
+[arguments-assert,vernacular]
 The command has indeed failed with message:
 Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index b6fbeb6ec7..e42c983361 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,5 +1,5 @@
 Fail Arguments eq_refl {B y}, [B] y.
-Fail Arguments identity T _ _.
+Arguments identity T _ _.
 Arguments eq_refl A x : assert.
 Arguments eq_refl {B y}, [B] y : rename.
 
-- 
cgit v1.2.3


From edb55a94fc5c0473e57f5a61c0c723194c2ff414 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 27 Sep 2016 17:15:10 +0200
Subject: Fix bug #4798: compat notations should not modify the parser.

This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
---
 test-suite/bugs/closed/4798.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/4798.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v
new file mode 100644
index 0000000000..dbc3d46fce
--- /dev/null
+++ b/test-suite/bugs/closed/4798.v
@@ -0,0 +1,3 @@
+Check match 2 with 0 => 0 | S n => n end.
+Notation "|" := 1 (compat "8.4").
+Check match 2 with 0 => 0 | S n => n end. (* fails *)
-- 
cgit v1.2.3


From 46daf37ed46397b03a30fa2d89b62ffcc2c8d166 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 29 Sep 2016 14:32:50 -0400
Subject: Set the default LtacProf cutoff to 2%

This was the original value from Tobias' code.  When a user passes
-profile-ltac on the command line, or inserts [Show Ltac Profile] in the
document, the most useful default behavior is to not overload them with
useless information.  When GUI clients want to display fancier profiling
information, there is no cost to the user to requiring them to specify
what cutoff they want.  If the GUI client does not have any special
LtacProf handling, the most useful presentation is again the one that
cuts off the display at 2% total time.
---
 test-suite/Makefile                      | 2 +-
 test-suite/output-modulo-time/ltacprof.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index a40ea80ae4..d2899034b8 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -51,7 +51,7 @@ SINGLE_QUOTE="
 get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
 # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
 has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
-has_profile_ltac_or_compile_flag = $(filter "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
+has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
 get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command))
 
 
diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v
index d79451f0f7..6611db70e2 100644
--- a/test-suite/output-modulo-time/ltacprof.v
+++ b/test-suite/output-modulo-time/ltacprof.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *)
+(* -*- coq-prog-args: ("-emacs" "-profile-ltac-cutoff" "0.0") -*- *)
 Ltac sleep' := do 100 (do 100 (do 100 idtac)).
 Ltac sleep := sleep'.
 
-- 
cgit v1.2.3


From c4c7aa6d7b14a6d76c287b97d487abe055406577 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 29 Sep 2016 18:28:24 -0400
Subject: LtacProf cutoff is for total percent, not time

---
 test-suite/Makefile                               |  4 +--
 test-suite/output-modulo-time/ltacprof_cutoff.out | 33 +++++++++++++++++++++++
 test-suite/output-modulo-time/ltacprof_cutoff.v   | 12 +++++++++
 3 files changed, 47 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/output-modulo-time/ltacprof_cutoff.out
 create mode 100644 test-suite/output-modulo-time/ltacprof_cutoff.v

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index a40ea80ae4..e3800ee22e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -304,12 +304,12 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
 	    | grep -v "^<W>" \
-	    | sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \
+	    | sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \
 	          -e 's/\s*0\.\s*//g' \
 		  -e 's/\s*[-+]nan\s*//g' \
 		  -e 's/\s*[-+]inf\s*//g' \
 	    > $$tmpoutput; \
-	  sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \
+	  sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \
 		-e 's/\s*0\.\s*//g' \
 		-e 's/\s*[-+]nan\s*//g' \
 		-e 's/\s*[-+]inf\s*//g' \
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out
new file mode 100644
index 0000000000..13cd87b8c2
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.out
@@ -0,0 +1,33 @@
+total time:      1.584s
+
+ tactic                                   local  total   calls       max 
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep --------------------------------- 100.0% 100.0%       3    0.572s
+─foo2 ----------------------------------   0.0% 100.0%       1    1.584s
+─foo1 ----------------------------------   0.0%  63.9%       1    1.012s
+
+ tactic                                   local  total   calls       max 
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─foo2 ----------------------------------   0.0% 100.0%       1    1.584s
+└foo1 ----------------------------------   0.0%  63.9%       1    1.012s
+
+total time:      1.584s
+
+ tactic                                   local  total   calls       max 
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep --------------------------------- 100.0% 100.0%       3    0.572s
+─foo2 ----------------------------------   0.0% 100.0%       1    1.584s
+─foo1 ----------------------------------   0.0%  63.9%       1    1.012s
+─foo0 ----------------------------------   0.0%  31.3%       1    0.496s
+─constructor ---------------------------   0.0%   0.0%       1    0.000s
+
+ tactic                                   local  total   calls       max 
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─foo2 ----------------------------------   0.0% 100.0%       1    1.584s
+ ├─foo1 --------------------------------   0.0%  63.9%       1    1.012s
+ │ ├─sleep -----------------------------  32.6%  32.6%       1    0.516s
+ │ └─foo0 ------------------------------   0.0%  31.3%       1    0.496s
+ │  └sleep -----------------------------  31.3%  31.3%       1    0.496s
+ └─sleep -------------------------------  36.1%  36.1%       1    0.572s
+─constructor ---------------------------   0.0%   0.0%       1    0.000s
+
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v
new file mode 100644
index 0000000000..50131470eb
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.v
@@ -0,0 +1,12 @@
+(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *)
+Require Coq.ZArith.BinInt.
+Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac).
+
+Ltac foo0 := idtac; sleep.
+Ltac foo1 := sleep; foo0.
+Ltac foo2 := sleep; foo1.
+Goal True.
+  foo2.
+  Show Ltac Profile CutOff 47.
+  constructor.
+Qed.
-- 
cgit v1.2.3


From 844b076bf5150a107d31cd4648955c3a6538a34b Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Wed, 28 Sep 2016 10:40:54 +0200
Subject: Fix #4762.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v
new file mode 100644
index 0000000000..7a87b07a8e
--- /dev/null
+++ b/test-suite/bugs/closed/4762.v
@@ -0,0 +1,24 @@
+Inductive myand (P Q : Prop) := myconj : P -> Q -> myand P Q.
+
+Lemma foo P Q R : R = myand P Q -> P -> Q -> R.
+Proof. intros ->; constructor; auto. Qed.
+
+Hint Extern 0 (myand _ _) => eapply foo; [reflexivity| |] : test1.
+
+Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R).
+Proof.
+  intros.
+  eauto with test1.
+Qed.
+
+Hint Extern 0 =>
+  match goal with
+  | |- myand _ _ => eapply foo; [reflexivity| |]
+  end : test2.
+
+Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R).
+Proof.
+  intros.
+  eauto with test2. (* works *)
+Qed.
+
-- 
cgit v1.2.3


From 775b8f28562d1d5063da2b28a06e59610b76f06f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 30 Sep 2016 10:14:10 +0200
Subject: Ignore file names in warning emitted by test-suite/output/* (#5111)

---
 test-suite/Makefile                      |  2 +-
 test-suite/output/Arguments_renaming.out | 18 +++++++++---------
 2 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index a40ea80ae4..6ecc7bcaad 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -280,7 +280,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
-	    | grep -v "^<W>" \
+	    | sed 's/File "[^"]*"/File "stdin"/' \
 	    > $$tmpoutput; \
 	  diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 815305581c..1633ad9765 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,20 +1,20 @@
-File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 1, characters 0-36:
+File "stdin", line 1, characters 0-36:
 Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
-[arguments-assert,vernacular]
+[arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
 Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
-File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25:
+File "stdin", line 2, characters 0-25:
 Warning: Ignoring rename of A into T. Only implicit arguments can be renamed.
-[arguments-assert,vernacular]
-File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25:
+[arguments-ignore-rename-nonimpl,vernacular]
+File "stdin", line 2, characters 0-25:
 Warning: This command is just asserting the number and names of arguments of
 identity. If this is what you want add ': assert' to silence the warning. If
 you want to clear implicit arguments add ': clear implicits'. If you want to
 clear notation scopes add ': clear scopes' [arguments-assert,vernacular]
-File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 4, characters 0-40:
+File "stdin", line 4, characters 0-40:
 Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
-[arguments-assert,vernacular]
+[arguments-ignore-rename-nonimpl,vernacular]
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
@@ -121,9 +121,9 @@ The command has indeed failed with message:
 Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
 Error: Extra argument y.
-File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 53, characters 0-26:
+File "stdin", line 53, characters 0-26:
 Warning: Ignoring rename of x into s. Only implicit arguments can be renamed.
-[arguments-assert,vernacular]
+[arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
 Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
-- 
cgit v1.2.3


From 69d43e7615f080c2e4e57a87e84b51be857ab678 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 30 Sep 2016 11:08:47 +0200
Subject: Restore code ignoring <W> lines in output (camlp5 warnings)

---
 test-suite/Makefile | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6ecc7bcaad..acf1dae059 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -280,6 +280,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
+	    | grep -v "^<W>" \
 	    | sed 's/File "[^"]*"/File "stdin"/' \
 	    > $$tmpoutput; \
 	  diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \
-- 
cgit v1.2.3


From c78af970e1f003587fba9bebdf3ab5ca3b23face Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 30 Sep 2016 12:16:01 +0200
Subject: Fix test-suite.

Restore subst output test file modified by mistake.
---
 test-suite/output/subst.out | 208 --------------------------------------------
 test-suite/output/subst.v   |  11 ---
 2 files changed, 219 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
index dbb9e09a43..209b2bc26f 100644
--- a/test-suite/output/subst.out
+++ b/test-suite/output/subst.out
@@ -26,19 +26,6 @@
   True
 1 subgoal
   
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
   x, y : nat
   Hx : x = 0
   Hy : y = 0
@@ -52,45 +39,6 @@
   True
 1 subgoal
   
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
-  x, z : nat
-  Hx : x = 0
-  Hz : z = 0
-  H1 : x = 1
-  HA : True
-  H2 : x = 2
-  H3 : 0 = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
   H1 : 0 = 1
   HA : True
   H2 : 0 = 2
@@ -101,58 +49,6 @@
   True
 1 subgoal
   
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
-  x, z : nat
-  Hx : x = 0
-  Hz : z = 0
-  H1 : x = 1
-  HA : True
-  H2 : x = 2
-  H3 : 0 = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
   y, z : nat
   Hy : y = 0
   Hz : z = 0
@@ -179,19 +75,6 @@
   True
 1 subgoal
   
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
-1 subgoal
-  
   x, y : nat
   Hx : x = 0
   Hy : y = 0
@@ -205,45 +88,6 @@
   True
 1 subgoal
   
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
-1 subgoal
-  
-  x, z : nat
-  Hx : x = 0
-  Hz : z = 0
-  H1 : x = 1
-  HA : True
-  H2 : x = 2
-  HB : True
-  H4 : z = 4
-  H3 : 0 = 3
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
-1 subgoal
-  
   HA, HB : True
   H4 : 0 = 4
   H3 : 0 = 3
@@ -251,55 +95,3 @@
   H2 : 0 = 2
   ============================
   True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
-1 subgoal
-  
-  x, z : nat
-  Hx : x = 0
-  Hz : z = 0
-  H1 : x = 1
-  HA : True
-  H2 : x = 2
-  HB : True
-  H4 : z = 4
-  H3 : 0 = 3
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v
index 91bdd03e02..e48aa6bb28 100644
--- a/test-suite/output/subst.v
+++ b/test-suite/output/subst.v
@@ -45,15 +45,4 @@ Show.
 trivial.
 Qed.
 
-(* A bug revealed by OCaml 4.03 warnings *)
-Goal forall y, let x:=0 in y=x -> y=y.
-intros * H;
-subst.
-Fail clear H. (* Was working *)
-Abort.
 
-Goal forall y, let x:=0 in y=x -> y=y.
-intros * H;
-subst.
-Fail clear H. (* Was failing before fix *)
-Abort.
-- 
cgit v1.2.3


From 98da77db53b4a41062c47f8f55418eb1fbb7e5bb Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 30 Sep 2016 16:19:45 +0200
Subject: test-suite/output-modulo-time made more robust

Order of items made stable
---
 test-suite/Makefile                               | 5 ++++-
 test-suite/output-modulo-time/ltacprof_cutoff.out | 4 +---
 2 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index efa0236c35..b32071e802 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -309,12 +309,15 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	          -e 's/\s*0\.\s*//g' \
 		  -e 's/\s*[-+]nan\s*//g' \
 		  -e 's/\s*[-+]inf\s*//g' \
+		  -e 's/^[^a-zA-Z]*//' \
+	    | sort \
 	    > $$tmpoutput; \
 	  sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \
 		-e 's/\s*0\.\s*//g' \
 		-e 's/\s*[-+]nan\s*//g' \
 		-e 's/\s*[-+]inf\s*//g' \
-	       $*.out > $$tmpexpected; \
+		-e 's/^[^a-zA-Z]*//' \
+	       $*.out | sort > $$tmpexpected; \
 	  diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out
index 13cd87b8c2..0cd5777ccf 100644
--- a/test-suite/output-modulo-time/ltacprof_cutoff.out
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.out
@@ -2,8 +2,8 @@ total time:      1.584s
 
  tactic                                   local  total   calls       max 
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─sleep --------------------------------- 100.0% 100.0%       3    0.572s
 ─foo2 ----------------------------------   0.0% 100.0%       1    1.584s
+─sleep --------------------------------- 100.0% 100.0%       3    0.572s
 ─foo1 ----------------------------------   0.0%  63.9%       1    1.012s
 
  tactic                                   local  total   calls       max 
@@ -19,7 +19,6 @@ total time:      1.584s
 ─foo2 ----------------------------------   0.0% 100.0%       1    1.584s
 ─foo1 ----------------------------------   0.0%  63.9%       1    1.012s
 ─foo0 ----------------------------------   0.0%  31.3%       1    0.496s
-─constructor ---------------------------   0.0%   0.0%       1    0.000s
 
  tactic                                   local  total   calls       max 
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
@@ -29,5 +28,4 @@ total time:      1.584s
  │ └─foo0 ------------------------------   0.0%  31.3%       1    0.496s
  │  └sleep -----------------------------  31.3%  31.3%       1    0.496s
  └─sleep -------------------------------  36.1%  36.1%       1    0.572s
-─constructor ---------------------------   0.0%   0.0%       1    0.000s
 
-- 
cgit v1.2.3


From 024cf5ae087024399cc894b121437d72cd11b480 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 30 Sep 2016 16:42:54 +0200
Subject: Fix bug #4471: [generalize dependent] permits ill-typed terms in
 trunk.

This bug was introduced by 37ab45726, because the new apply_type function
was not checking that the new goal was indeed well-typed. We add this check
locally in the generalize dependent tactic.
---
 test-suite/bugs/closed/4471.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/4471.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4471.v b/test-suite/bugs/closed/4471.v
new file mode 100644
index 0000000000..36efc42d47
--- /dev/null
+++ b/test-suite/bugs/closed/4471.v
@@ -0,0 +1,6 @@
+Goal forall (A B : Type) (P : forall _ : prod A B, Type) (a : A) (b : B) (p p0 : forall (x : A) (x' : B), P (@pair A B x x')),
+    @eq (P (@pair A B a b)) (p (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b)))
+        (p0 (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b))).
+Proof.
+  intros.
+  Fail generalize dependent (a, b).
-- 
cgit v1.2.3


From 064de6f6839c4ef963b83018812c5d4113eb2bb9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 30 Sep 2016 17:25:58 +0200
Subject: Fix bug #5045: [generalize] creates ill-typed terms in 8.6.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5045.v b/test-suite/bugs/closed/5045.v
new file mode 100644
index 0000000000..dc38738d8f
--- /dev/null
+++ b/test-suite/bugs/closed/5045.v
@@ -0,0 +1,3 @@
+Axiom silly : 1 = 1 -> nat -> nat.
+Goal forall pf : 1 = 1, silly pf 0 = 0 -> True.
+  Fail generalize (@eq nat).
-- 
cgit v1.2.3


From acbe712fd643516ff63ecfe3e106deb695dbd9b3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Oct 2016 21:37:16 +0200
Subject: Fix bug #4661: Cannot mask the absolute name.

The patch is quite dumb: it essentially consists in alpha-renaming bound
module names when printing a functor, by checking that the name was not
already present, and generating a fresh one otherwise.
---
 test-suite/bugs/closed/4661.v     | 10 ++++++++++
 test-suite/output/PrintModule.out |  1 +
 test-suite/output/PrintModule.v   | 16 ++++++++++++++++
 3 files changed, 27 insertions(+)
 create mode 100644 test-suite/bugs/closed/4661.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4661.v b/test-suite/bugs/closed/4661.v
new file mode 100644
index 0000000000..03d2350a69
--- /dev/null
+++ b/test-suite/bugs/closed/4661.v
@@ -0,0 +1,10 @@
+Module Type Test.
+  Parameter t : Type.
+End Test.
+
+Module Type Func (T:Test).
+  Parameter x : Type.
+End Func.
+
+Module Shortest_path (T : Test).
+Print Func.
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index db464fd07e..751d5fcc48 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -2,3 +2,4 @@ Module N : S with Definition T := nat := M
 
 Module N : S with Module T := K := M
 
+Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 999d9a9862..5f30f7cda6 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -32,3 +32,19 @@ Module N : S with Module T := K := M.
 Print Module N.
 
 End BAR.
+
+Module QUX.
+
+Module Type Test.
+  Parameter t : Type.
+End Test.
+
+Module Type Func (T:Test).
+  Parameter x : T.t.
+End Func.
+
+Module Shortest_path (T : Test).
+Print Func.
+End Shortest_path.
+
+End QUX.
-- 
cgit v1.2.3