From 12f1c409daf2cdbd7d0323f0d61723819532b362 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 16:56:25 +0200
Subject: Really fixing #2602 which was wrongly working because of #5487 hiding
 the cause.

The cause was a missing evar/evar clause in ltac pattern-matching
function (constr_matching.ml).
---
 test-suite/success/ltac.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index ce90990594..d7ec092d76 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.
-- 
cgit v1.2.3


From f6856c5022ef27cdc492daadd1301cfcad025b01 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 1 May 2017 11:34:00 -0400
Subject: remove unneeded -emacs flag to coq-prog-args

---
 test-suite/success/Compat84.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/success')

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.
-- 
cgit v1.2.3


From cea40f37ab638031b9d5c6434ee5651a16ea1f3e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 09:04:17 +0200
Subject: Fixing Set Rewriting Schemes bugs introduced in v8.5.

- Fixing a typo introduced in 31dbba5f.
- Adapting to computation of universe constraints in pretyping.
- Adding a regression test.
---
 test-suite/success/Scheme.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'test-suite/success')

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.
-- 
cgit v1.2.3


From e2de94b90e8802fa5c5dc33c7daf6b8ce5646bfa Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 14 May 2017 00:10:57 +0200
Subject: Fixing a bug with nested "as" clauses in "match".

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

(limited to 'test-suite/success')

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.
-- 
cgit v1.2.3