12 files changed, 144 insertions, 5 deletions
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/Cases.v b/test-suite/success/Cases.v
index 49c465b6c6..52fe98ac07 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1868,3 +1868,8 @@ Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
 Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end.
 
 Check match niln in listn O return O=O with niln => eq_refl end.
+
+(* A test about nested "as" clauses *)
+(* (was failing up to May 2017) *)
+
+Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end.
diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
index db6348fa17..732a024fc1 100644
--- a/test-suite/success/Compat84.v
+++ b/test-suite/success/Compat84.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
 
 Goal True.
   solve [ constructor 1 ]. Undo.
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/Scheme.v b/test-suite/success/Scheme.v
index dd5aa81d1d..855f26698c 100644
--- a/test-suite/success/Scheme.v
+++ b/test-suite/success/Scheme.v
@@ -2,3 +2,26 @@
 
 Scheme Induction for eq Sort Prop.
 Check eq_ind_dep.
+
+(* This was broken in v8.5 *)
+
+Set Rewriting Schemes.
+Inductive myeq A (a:A) : A -> Prop := myrefl : myeq A a a.
+Unset Rewriting Schemes.
+
+Check myeq_rect.
+Check myeq_ind.
+Check myeq_rec.
+Check myeq_congr.
+Check myeq_sym_internal.
+Check myeq_rew.
+Check myeq_rew_dep.
+Check myeq_rew_fwd_dep.
+Check myeq_rew_r.
+Check internal_myeq_sym_involutive.
+Check myeq_rew_r_dep.
+Check myeq_rew_fwd_r_dep.
+
+Set Rewriting Schemes.
+Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true.
+Unset Rewriting Schemes.
diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v
new file mode 100644
index 0000000000..fafe272925
--- /dev/null
+++ b/test-suite/success/boundvars.v
@@ -0,0 +1,14 @@
+(* An example showing a bug in the detection of free variables *)
+(* "x" is not free in the common type of "x" and "y" *)
+
+Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.
+
+(* An example showing a bug in the detection of bound variables *)
+
+Goal forall x, match x return x = x with 0 => eq_refl | _ => eq_refl end = eq_refl.
+intro.
+match goal with
+|- (match x as y in nat return y = y with O => _ | S n => _ end) = _ => assert (forall y, y = 0) end.
+intro.
+Check x0. (* Check that "y" has been bound to "x0" while matching "match x as x0 return x0=x0 with ... end" *)
+Abort.
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index 1f0b7d38a9..a9821b027f 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -59,3 +59,12 @@ unfold x.
 (* check that n in 0+n is not interpreted as the n from "fun n" *)
 change n with (0+n).
 Abort.
+
+(* Check non-collision of non-normalized defined evars with pattern variables *)
+
+Goal exists x, 1=1 -> x=1/\x=1.
+eexists ?[n]; intros; split.
+eassumption.
+match goal with |- ?x=1 => change (x=1) with (0+x=1) end.
+match goal with |- 0+1=1 => trivial end.
+Qed.
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 12ddbda84e..f5bb884d27 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -15,7 +15,7 @@ Proof.
   intros n H.
   dependent destruction H.
   assumption.
-Save.
+Qed.
 
 Require Import ProofIrrelevance.
 
@@ -25,7 +25,7 @@ Proof.
   dependent destruction v.
   exists v ; exists a.
   reflexivity.
-Save.
+Qed.
 
 (* Extraction Unnamed_thm. *)
 
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index ce90990594..1d35f1ef6c 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -317,3 +317,23 @@ let T := constr:(fun a b : nat => a) in
   end.
 exact (eq_refl n).
 Qed.
+
+(* A variant of #2602 which was wrongly succeeding because "a", bound to
+   "?m", was then internally turned into a "_" in the second matching *)
+
+Goal exists m, S m > 0.
+eexists.
+Fail match goal with
+ | |- context [ S ?a ] =>
+     match goal with
+       | |- S a > a => idtac
+     end
+end.
+Abort.
+
+(* Test evar syntax *)
+
+Goal True.
+evar (0=0).
+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/transparent_abstract.v b/test-suite/success/transparent_abstract.v
new file mode 100644
index 0000000000..ff4509c4a8
--- /dev/null
+++ b/test-suite/success/transparent_abstract.v
@@ -0,0 +1,21 @@
+Class by_transparent_abstract {T} (x : T) := make_by_transparent_abstract : T.
+Hint Extern 0 (@by_transparent_abstract ?T ?x) => change T; transparent_abstract exact_no_check x : typeclass_instances.
+
+Goal True /\ True.
+Proof.
+  split.
+  transparent_abstract exact I using foo.
+  let x := (eval hnf in foo) in constr_eq x I.
+  let x := constr:(ltac:(constructor) : True) in
+  let T := type of x in
+  let x := constr:(_ : by_transparent_abstract x) in
+  let x := (eval cbv delta [by_transparent_abstract] in (let y : T := x in y)) in
+  pose x as x'.
+  simpl in x'.
+  let v := eval cbv [x'] in x' in tryif constr_eq v I then fail 0 else idtac.
+  hnf in x'.
+  let v := eval cbv [x'] in x' in tryif constr_eq v I then idtac else fail 0.
+  exact x'.
+Defined.
+Check eq_refl : I = foo.
+Eval compute in foo.
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 296686e16e..6f7498d659 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -188,3 +188,14 @@ Proof.
   apply idpath.
   apply idpath.
 Defined.
+
+(* An example where it is necessary to evar-normalize the instance of
+   an evar to evaluate if it is a pattern *)
+
+Check
+  let a := ?[P] in
+  fun (H : forall y (P : nat -> Prop), y = 0 -> P y)
+      x (p:x=0) =>
+    H ?[y] a p : x = 0.
+(* We have to solve "?P ?y[x] == x = 0" knowing from
+   "p : (x=0) == (?y[x] = 0)" that "?y := x" *)