From 32a9a4e3656e581af41c26f48f63ed1daec331d8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 May 2015 18:54:18 +0200
Subject: Fixing treatment of recursive equations damaged by 857e82b2ca0d1.
 Improving treatment of recursive equations compared to 8.4 (see test-suite).
 Experimenting not to unfold local defs ever in subst. (+ Slight
 simplification in checking reflexive equalities only once).

---
 test-suite/success/subst.v | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 test-suite/success/subst.v

(limited to 'test-suite')

diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v
new file mode 100644
index 0000000000..8336f6a806
--- /dev/null
+++ b/test-suite/success/subst.v
@@ -0,0 +1,25 @@
+(* Test various subtleties of the "subst" tactics *)
+
+(* Should proceed from left to right (see #4222) *)
+Goal forall x y, x = y -> x = 3 -> y = 2 -> x = y.
+intros.
+subst.
+change (3 = 2) in H1.
+change (3 = 3).
+Abort.
+
+(* Should work with "x = y" and "x = t" equations (see #4214, failed in 8.4) *)
+Goal forall x y, x = y -> x = 3 -> x = y.
+intros.
+subst.
+change (3 = 3).
+Abort.
+
+(* Should substitute cycles once, until a recursive equation is obtained *)
+(* (failed in 8.4) *)
+Goal forall x y, x = S y -> y = S x -> x = y.
+intros.
+subst.
+change (y = S (S y)) in H0.
+change (S y = y).
+Abort.
-- 
cgit v1.2.3


From 5cbc018fe934750bdf1043da68f99911be4ee6f6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 5 May 2015 19:25:24 +0200
Subject: Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for
 preserving compatibility of subst after #4214 being solved.

---
 test-suite/bugs/closed/4214.v | 5 -----
 test-suite/bugs/opened/4214.v | 5 +++++
 2 files changed, 5 insertions(+), 5 deletions(-)
 delete mode 100644 test-suite/bugs/closed/4214.v
 create mode 100644 test-suite/bugs/opened/4214.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/closed/4214.v
deleted file mode 100644
index cd53c898e9..0000000000
--- a/test-suite/bugs/closed/4214.v
+++ /dev/null
@@ -1,5 +0,0 @@
-(* Check that subst uses all equations around *)
-Goal forall A (a b c : A), b = a -> b = c -> a = c.
-intros.
-subst.
-reflexivity.
diff --git a/test-suite/bugs/opened/4214.v b/test-suite/bugs/opened/4214.v
new file mode 100644
index 0000000000..cd53c898e9
--- /dev/null
+++ b/test-suite/bugs/opened/4214.v
@@ -0,0 +1,5 @@
+(* Check that subst uses all equations around *)
+Goal forall A (a b c : A), b = a -> b = c -> a = c.
+intros.
+subst.
+reflexivity.
-- 
cgit v1.2.3


From 39a67d502d341562b68c0f52163b2863bdd5ebd4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 9 May 2015 18:04:40 +0200
Subject: Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by
 default).

---
 test-suite/bugs/opened/4214.v |  2 +-
 test-suite/success/subst.v    | 25 -------------------------
 2 files changed, 1 insertion(+), 26 deletions(-)
 delete mode 100644 test-suite/success/subst.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/opened/4214.v b/test-suite/bugs/opened/4214.v
index cd53c898e9..3daf452132 100644
--- a/test-suite/bugs/opened/4214.v
+++ b/test-suite/bugs/opened/4214.v
@@ -2,4 +2,4 @@
 Goal forall A (a b c : A), b = a -> b = c -> a = c.
 intros.
 subst.
-reflexivity.
+Fail reflexivity.
diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v
deleted file mode 100644
index 8336f6a806..0000000000
--- a/test-suite/success/subst.v
+++ /dev/null
@@ -1,25 +0,0 @@
-(* Test various subtleties of the "subst" tactics *)
-
-(* Should proceed from left to right (see #4222) *)
-Goal forall x y, x = y -> x = 3 -> y = 2 -> x = y.
-intros.
-subst.
-change (3 = 2) in H1.
-change (3 = 3).
-Abort.
-
-(* Should work with "x = y" and "x = t" equations (see #4214, failed in 8.4) *)
-Goal forall x y, x = y -> x = 3 -> x = y.
-intros.
-subst.
-change (3 = 3).
-Abort.
-
-(* Should substitute cycles once, until a recursive equation is obtained *)
-(* (failed in 8.4) *)
-Goal forall x y, x = S y -> y = S x -> x = y.
-intros.
-subst.
-change (y = S (S y)) in H0.
-change (S y = y).
-Abort.
-- 
cgit v1.2.3


From 7bc1610376fac29397be39d4a06b178e8e35e66e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 May 2015 11:17:54 +0200
Subject: Test for bug #4232.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4232.v b/test-suite/bugs/closed/4232.v
new file mode 100644
index 0000000000..61e544a914
--- /dev/null
+++ b/test-suite/bugs/closed/4232.v
@@ -0,0 +1,20 @@
+Require Import Setoid Morphisms Vector.
+
+Class Equiv A := equiv : A -> A -> Prop.
+Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).
+
+Global Declare Instance vec_equiv {A} `{Equiv A} {n}: Equiv (Vector.t A n).
+Global Declare Instance vec_setoid A `{Setoid A} n : Setoid (Vector.t A n).
+
+Global Declare Instance tl_proper1 {A} `{Equiv A} n:
+  Proper ((equiv) ==> (equiv))
+         (@tl A n).
+
+Lemma test:
+  forall {A} `{Setoid A} n (xa ya: Vector.t A (S n)),
+    (equiv xa ya) -> equiv (tl xa) (tl ya).
+Proof.
+  intros A R HA n xa ya Heq.
+  setoid_rewrite Heq.
+  reflexivity.
+Qed.
-- 
cgit v1.2.3


From 20fd4f91c5096d2f9c06f2bdca23127be4d81aad Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2015 14:17:45 +0200
Subject: Test for bug #4234.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4234.v b/test-suite/bugs/closed/4234.v
new file mode 100644
index 0000000000..348dd49d93
--- /dev/null
+++ b/test-suite/bugs/closed/4234.v
@@ -0,0 +1,7 @@
+Definition UU := Type.
+
+Definition dirprodpair {X Y : UU} := existT (fun x : X => Y).
+
+Definition funtoprodtoprod {X Y Z : UU} : { a : X -> Y & X -> Z }.
+Proof.
+  refine (dirprodpair _ (fun x => _)).
-- 
cgit v1.2.3


From 95b4a54ec6a9aacffe8c11df1b443d36b9f6dda7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 12 May 2015 16:48:01 +0200
Subject: Extraction: fix the detection of the "polyprop" situation

 The ~polyprop argument wasn't propagated properly anymore,
 leading the extraction to try to operate on situations it cannot
 handle (yet). Cf Table.error_singleton_become_prop for more details.

 Regression test added.
---
 test-suite/success/extraction_polyprop.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/success/extraction_polyprop.v

(limited to 'test-suite')

diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v
new file mode 100644
index 0000000000..7215bd9905
--- /dev/null
+++ b/test-suite/success/extraction_polyprop.v
@@ -0,0 +1,11 @@
+(* The current extraction cannot handle this situation,
+   and shouldn't try, otherwise it might produce some Ocaml
+   code that segfaults. See Table.error_singleton_become_prop
+   or S. Glondu's thesis for more details. *)
+
+Definition f {X} (p : (nat -> X) * True) : X * nat :=
+  (fst p 0, 0).
+
+Definition f_prop := f ((fun _ => I),I).
+
+Fail Extraction f_prop.
-- 
cgit v1.2.3


From 574b4096517b4ac9189c2226e1cd75745e788db0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 May 2015 09:11:22 +0200
Subject: Better fixing #4198 such that the term to match is looked for before
 the predicate, thus respecting the visual left-to-right top-down order (see
 a45bd5981092).

This fixes CFGV.
---
 test-suite/bugs/closed/4198.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
index ef991365d5..f85a60264d 100644
--- a/test-suite/bugs/closed/4198.v
+++ b/test-suite/bugs/closed/4198.v
@@ -1,3 +1,5 @@
+(* Check that the subterms of the predicate of a match are taken into account *)
+
 Require Import List.
 Open Scope list_scope.
 Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
@@ -11,3 +13,25 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
   match goal with
     | [ |- appcontext G[@hd] ] => idtac
   end.
+
+(* This second example comes from CFGV where inspecting subterms of a
+   match is expecting to inspect first the term to match (even though
+   it would certainly be better to provide a "match x with _ end"
+   construct for generically matching a "match") *)
+
+Ltac find_head_of_head_match T :=
+  match T with context [?E] => 
+    match T with  
+    | E => fail 1 
+    | _ => constr:(E) 
+    end 
+  end.
+
+Ltac mydestruct :=
+  match goal with 
+  | |- ?T1 = _ => let E := find_head_of_head_match T1 in destruct E
+  end.
+
+Goal forall x, match x with 0 => 0 | _ => 0 end = 0.
+intros.
+mydestruct.
-- 
cgit v1.2.3


From d91addb140ba7315d70c4599b0d058bef798ac1c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2015 23:38:55 +0200
Subject: Fixing bug #4216:

Internal error: Anomaly: Uncaught exception Not_found. Please report.

An evarmap was lost because of an unsound typing primitive.
---
 test-suite/bugs/closed/4216.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 test-suite/bugs/closed/4216.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4216.v b/test-suite/bugs/closed/4216.v
new file mode 100644
index 0000000000..ae7f746778
--- /dev/null
+++ b/test-suite/bugs/closed/4216.v
@@ -0,0 +1,20 @@
+Generalizable Variables T A.
+
+Inductive path `(a: A): A -> Type := idpath: path a a.
+
+Class TMonad (T: Type -> Type) := {
+  bind: forall {A B: Type}, (T A) -> (A -> T B) -> T B;
+  ret: forall {A: Type}, A -> T A;
+  ret_unit_left: forall {A B: Type} (k: A -> T B) (a: A),
+                 path (bind (ret a) k) (k a)
+  }.
+
+Let T_fzip `{TMonad T} := fun (A B: Type) (f: T (A -> B)) (t: T A)
+                  => bind t (fun a => bind f (fun g => ret (g a) )).
+Let T_pure `{TMonad T} := @ret _ _.
+
+Let T_pure_id `{TMonad T} {A: Type} (t: A -> A) (x: T A): 
+        path (T_fzip A A (T_pure (A -> A) t) x) x.
+  unfold T_fzip, T_pure.
+  Fail rewrite (ret_unit_left (fun g a => ret (g a)) (fun x => x)).
+
-- 
cgit v1.2.3