Merge branch 'v8.6'

4 files changed, 42 insertions, 1 deletions

diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 49c465b6c..52fe98ac0 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 db6348fa1..732a024fc 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/Scheme.v b/test-suite/success/Scheme.v
index dd5aa81d1..855f26698 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/ltac.v b/test-suite/success/ltac.v
index ce9099059..d7ec092d7 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -317,3 +317,16 @@ 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.