21 files changed, 258 insertions, 6 deletions
diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v
new file mode 100644
index 0000000000..4aef5bb95e
--- /dev/null
+++ b/test-suite/bugs/closed/4306.v
@@ -0,0 +1,32 @@
+Require Import List.
+Require Import Arith.
+Require Import Recdef. 
+Require Import Omega.
+
+Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
+  match xys with
+    | (nil, _) => snd xys
+    | (_, nil) => fst xys
+    | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+                                | Lt => x :: foo (xs', y :: ys')
+                                | Eq => x :: foo (xs', ys')
+                                | Gt => y :: foo (x :: xs', ys')
+                              end
+  end.
+Proof.
+  intros; simpl; omega.
+  intros; simpl; omega.
+  intros; simpl; omega.
+Qed.
+
+Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
+  let (xs, ys) := xys in
+  match (xs, ys) with
+    | (nil, _) => ys
+    | (_, nil) => xs
+    | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+                                | Lt => x :: foo (xs', ys)
+                                | Eq => x :: foo (xs', ys')
+                                | Gt => y :: foo (xs, ys')
+                              end
+  end.
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/5321.v b/test-suite/bugs/closed/5321.v
new file mode 100644
index 0000000000..03514e23b1
--- /dev/null
+++ b/test-suite/bugs/closed/5321.v
@@ -0,0 +1,18 @@
+Definition proj1_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
+  : proj1_sig u = proj1_sig v
+  := f_equal (@proj1_sig _ _) p.
+
+Definition proj2_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
+  : eq_rect _ _ (proj2_sig u) _ (proj1_sig_path p) = proj2_sig v
+  := match p with eq_refl => eq_refl end.
+
+Goal forall sz : nat,
+    let sz' := sz in
+    forall pf : sz = sz',
+      let feq_refl := exist (fun x : nat => sz = x) sz' eq_refl in
+      let fpf := exist (fun x : nat => sz = x) sz' pf in feq_refl = fpf -> 
+proj2_sig feq_refl = proj2_sig fpf.
+Proof.
+  intros.
+  etransitivity; [ | exact (proj2_sig_path H) ].
+  Fail clearbody fpf.
diff --git a/test-suite/bugs/closed/5377.v b/test-suite/bugs/closed/5377.v
new file mode 100644
index 0000000000..130d9f9abf
--- /dev/null
+++ b/test-suite/bugs/closed/5377.v
@@ -0,0 +1,54 @@
+Goal ((forall (t : Type) (x y : t),
+          True ->
+          x = y)) -> False.
+Proof.
+  intro HG.
+  let P := lazymatch goal with
+  | [ H : forall t x y, True -> @?P t x y
+                        |- _ ]
+    => P
+  end in
+  pose (f := P).
+  unify f (fun (t : Type) (x y : t) => x = y).
+Abort.
+
+Goal True.
+Proof.
+let c := lazymatch constr:(fun (T : nat -> Type) (y : nat) (_ : T y) => y) with
+         | fun _ y _ => @?C y => C
+         end in
+pose (f := c).
+unify f (fun n : nat => n).
+Abort.
+
+Goal (forall x : nat, x = x -> x = x \/ x = x) -> True.
+Proof.
+intro.
+let P := lazymatch goal with
+| [ H : forall y, @?P y -> @?P y \/ _ |- _ ]
+  => P
+end in
+pose (f := P).
+unify f (fun x : nat => x = x).
+Abort.
+
+Goal (forall x : nat, x = x -> x = x \/ x = x) -> True.
+Proof.
+intro.
+lazymatch goal with
+| [ H : forall y, @?P y -> @?Q y \/ _ |- _ ]
+  => idtac
+end.
+Abort.
+
+Axiom eq : forall {T} (_ : T), Prop.
+
+Goal forall _ : (forall t (_ : eq t) (x : t), eq x), Prop.
+Proof.
+intro.
+let P := lazymatch goal with
+| [ H : forall t _ x, @?P t x |- _ ]
+  => P
+end in
+pose (f := P).
+Abort.
diff --git a/test-suite/bugs/closed/5435.v b/test-suite/bugs/closed/5435.v
new file mode 100644
index 0000000000..60ace5ce96
--- /dev/null
+++ b/test-suite/bugs/closed/5435.v
@@ -0,0 +1,2 @@
+Definition foo (x : nat) := Eval native_compute in x.
+
diff --git a/test-suite/bugs/closed/5449.v b/test-suite/bugs/closed/5449.v
new file mode 100644
index 0000000000..d7fc2aaa00
--- /dev/null
+++ b/test-suite/bugs/closed/5449.v
@@ -0,0 +1,6 @@
+(* An example of decide equality which was failing due to a lhs dep into the rhs *)
+
+Require Import Coq.PArith.BinPos.
+Goal forall x y, {Pos.compare_cont Gt x y = Gt} + {Pos.compare_cont Gt x y <> Gt}.
+intros.
+decide equality.
diff --git a/test-suite/bugs/closed/5460.v b/test-suite/bugs/closed/5460.v
new file mode 100644
index 0000000000..50221cdd83
--- /dev/null
+++ b/test-suite/bugs/closed/5460.v
@@ -0,0 +1,11 @@
+(* Bugs in computing dependencies in pattern-matching compilation *)
+
+Inductive A := a1 | a2.
+Inductive B := b.
+Inductive C : A -> Type := c : C a1 | d : C a2.
+Definition P (x : A) (y : C x) (z : B) : nat :=
+  match z, x, y with
+      | b, a1, c => 0
+      | b, a2, d => 0
+      | _, _, _ => 1
+  end.
diff --git a/test-suite/bugs/closed/5469.v b/test-suite/bugs/closed/5469.v
new file mode 100644
index 0000000000..fce671c754
--- /dev/null
+++ b/test-suite/bugs/closed/5469.v
@@ -0,0 +1,3 @@
+(* Some problems with the special treatment of curly braces *)
+
+Reserved Notation "'a' { x }" (at level 0, format "'a' { x }").
diff --git a/test-suite/bugs/closed/5470.v b/test-suite/bugs/closed/5470.v
new file mode 100644
index 0000000000..5b3984b6df
--- /dev/null
+++ b/test-suite/bugs/closed/5470.v
@@ -0,0 +1,3 @@
+(* This used to raise an anomaly *)
+
+Fail Reserved Notation "x +++ y" (at level 70, x binder).
diff --git a/test-suite/bugs/closed/5476.v b/test-suite/bugs/closed/5476.v
new file mode 100644
index 0000000000..b2d9d943bc
--- /dev/null
+++ b/test-suite/bugs/closed/5476.v
@@ -0,0 +1,28 @@
+Require Setoid.
+
+Goal forall (P : Prop) (T : Type) (m m' : T) (T0 T1 : Type) (P2 : forall _ : 
+Prop, Prop) 
+            (P0 : Set) (x0 : P0) (P1 : forall (_ : P0) (_ : T), Prop)
+            (P3 : forall (_ : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (_ : 
+T) (_ : Prop), Prop)
+            (o : forall _ : P0, option T1)
+            (_ : P3
+                   (fun (k : P0) (_ : T0) (_ : Prop) =>
+                      match o k return Prop with
+                      | Some _ => True
+                      | None => False
+                      end) m' P) (_ : P2 (P1 x0 m))
+            (_ : forall (f : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (m1 m2 
+: T) 
+                        (k : P0) (e : T0) (_ : P2 (P1 k m1)), iff (P3 f m2 P) 
+(f k e (P3 f m1 P))), False.
+Proof.
+  intros ???????????? H0 H H1.
+  rewrite H1 in H0; eauto with nocore.
+  { lazymatch goal with
+    | H : match ?X with _ => _ end |- _
+      => first [ lazymatch goal with
+                 | [ H' : context[X] |- _ ] => idtac H
+                 end
+               | fail 1 "could not find" X ]
+    end.
diff --git a/test-suite/bugs/closed/5501.v b/test-suite/bugs/closed/5501.v
new file mode 100644
index 0000000000..24739a3658
--- /dev/null
+++ b/test-suite/bugs/closed/5501.v
@@ -0,0 +1,21 @@
+Set Universe Polymorphism.
+
+Record Pred@{A} :=
+  { car :> Type@{A}
+  ; P : car -> Prop
+  }.
+
+Class All@{A} (A : Pred@{A}) : Type :=
+  { proof : forall (a : A), P A a
+  }.
+
+Record Pred_All@{A} : Type :=
+  { P' :> Pred@{A}
+  ; P'_All : All P'
+  }.
+
+Global Instance Pred_All_instance (A : Pred_All) : All A := P'_All A.
+
+Definition Pred_All_proof {A : Pred_All} (a : A) : P A a.
+Proof.
+solve[auto using proof].
diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v
index b62f9b6867..bb9579d487 100644
--- a/test-suite/failure/proofirrelevance.v
+++ b/test-suite/failure/proofirrelevance.v
@@ -1,6 +1,5 @@
-(* This was working in version 8.1beta (bug in the Sort-polymorphism
-   of inductive types), but this is inconsistent with classical logic
-   in Prop *)
+(* This was working in version 8.1beta (bug in template polymorphism),
+   but this is inconsistent with classical logic in Prop *)
 
 Inductive bool_in_prop : Type := hide : bool -> bool_in_prop
 with bool : Type := true : bool | false : bool.
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index c012a86b01..95be04c32c 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -37,3 +37,5 @@ fun '(x, y) '(z, t) => swap (x, y) = (z, t)
      : A * B -> B * A -> Prop
 forall '(x, y) '(z, t), swap (x, y) = (z, t)
      : Prop
+fun (pat : nat) '(x, y) => x + y = pat
+     : nat -> nat * nat -> Prop
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 6fa357a90c..0bad472f41 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -64,3 +64,6 @@ Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
 Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
 
 End Suboptimal.
+
+(** Test risk of collision for internal name *)
+Check fun pat => fun '(x,y) => x+y = pat.
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 81fda176ec..7446c17d98 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -98,6 +98,14 @@ h: n <> newdef n
 h': newdef n <> n
 h: n <> newdef n
 h: n <> newdef n
+h: n <> newdef n
+h': newdef n <> n
+The command has indeed failed with message:
+No such goal.
+The command has indeed failed with message:
+Query commands only support the single numbered goal selector.
+The command has indeed failed with message:
+Query commands only support the single numbered goal selector.
 h: P n
 h': ~ P n
 h: P n
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index 2a0f0b407c..82096f29bf 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -10,11 +10,19 @@ Search (@eq _ _ _) true -false "prop" -"intro".  (* andb_prop *)
 Definition newdef := fun x:nat => x.
 
 Goal forall n:nat, n <> newdef n -> newdef n <> n -> False.
-  intros n h h'.
+  cut False.
+  intros _ n h h'.
   Search n.                             (* search hypothesis *)
   Search newdef.                        (* search hypothesis *)
   Search ( _ <> newdef _).              (* search hypothesis, pattern *)
   Search ( _ <> newdef _) -"h'".        (* search hypothesis, pattern *)
+
+  1:Search newdef.
+  2:Search newdef.
+
+  Fail 3:Search newdef.
+  Fail 1-2:Search newdef.
+  Fail all:Search newdef.
 Abort.
 
 Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v
index c29e529783..e59828defe 100644
--- a/test-suite/success/Case19.v
+++ b/test-suite/success/Case19.v
@@ -1,5 +1,5 @@
 (* This used to fail in Coq version 8.1 beta due to a non variable
-   universe (issued by the inductive sort-polymorphism) being sent by
+   universe (issued by template polymorphism) being sent by
    pretyping to the kernel (bug #1182) *)
 
 Variable T : Type.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index f702aa62f1..f07773f8bd 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -21,3 +21,9 @@ Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A
 (* Test sharing information between different hypotheses *)
 
 Parameters (a:_) (b:a=0).
+
+(* These examples were failing due to a lifting wrongly taking let-in into account *)
+
+Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.
+
+Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 52acad7460..837f2efd06 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -121,6 +121,7 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
 Goal True.
 {{ exact I. }}
 Qed.
+
 Check |- {{ 0 }} 0.
 
 (* Check parsing of { and } is not affected by notations #3479 *)
@@ -135,3 +136,9 @@ Notation "" := (@nil) (only printing).
 
 (* Check that a notation cannot be neither parsing nor printing. *)
 Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing).
+
+(* Check "where" clause for inductive types with parameters *)
+
+Reserved Notation "x === y" (at level 50).
+Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x
+ where "x === y" := (EQ x y).
diff --git a/test-suite/success/all-check.v b/test-suite/success/all-check.v
new file mode 100644
index 0000000000..391bc540e4
--- /dev/null
+++ b/test-suite/success/all-check.v
@@ -0,0 +1,3 @@
+Goal True.
+Fail all:Check _.
+Abort.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 878875bd92..66ff55edcb 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -321,4 +321,34 @@ Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
 Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
 Type)) eq_refl.
 
-End Hurkens'.
-\ No newline at end of file
+End Hurkens'.
+
+Module Anonymous.
+  Set Universe Polymorphism.
+
+  Definition defaultid := (fun x => x) : Type -> Type.
+  Definition collapseid := defaultid@{_ _}.
+  Check collapseid@{_}.
+
+  Definition anonid := (fun x => x) : Type -> Type@{_}.
+  Check anonid@{_}.
+
+  Definition defaultalg := (fun x : Type => x) (Type : Type).
+  Definition usedefaultalg := defaultalg@{_ _ _}.
+  Check usedefaultalg@{_ _}.
+
+  Definition anonalg := (fun x : Type@{_} => x) (Type : Type).
+  Check anonalg@{_ _}.
+
+  Definition unrelated@{i j} := nat.
+  Definition useunrelated := unrelated@{_ _}.
+  Check useunrelated@{_ _}.
+
+  Definition inthemiddle@{i j k} :=
+    let _ := defaultid@{i j} in
+    anonalg@{k j}.
+  (* i <= j < k *)
+  Definition collapsethemiddle := inthemiddle@{i _ j}.
+  Check collapsethemiddle@{_ _}.
+
+End Anonymous.
diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v
index db2bbb0dc7..07a5bc0606 100644
--- a/test-suite/success/record_syntax.v
+++ b/test-suite/success/record_syntax.v
@@ -45,3 +45,11 @@ Record Foo := { foo : unit; }.
 Definition foo_ := {| foo := tt; |}.
 
 End E.
+
+Module F.
+
+Record Foo := { foo : nat * nat -> nat -> nat }.
+
+Definition foo_ := {| foo '(x,y) n := x+y+n |}.
+
+End F.