Merge v8.5 into trunk

Conflicts:
	tactics/eauto.ml4

(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)

5 files changed, 72 insertions, 1 deletions

diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
index ef991365d..f85a60264 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.
diff --git a/test-suite/bugs/closed/4216.v b/test-suite/bugs/closed/4216.v
new file mode 100644
index 000000000..ae7f74677
--- /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)).
+
diff --git a/test-suite/bugs/closed/4232.v b/test-suite/bugs/closed/4232.v
new file mode 100644
index 000000000..61e544a91
--- /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.
diff --git a/test-suite/bugs/closed/4234.v b/test-suite/bugs/closed/4234.v
new file mode 100644
index 000000000..348dd49d9
--- /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 => _)).
diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/opened/4214.v
index cd53c898e..3daf45213 100644
--- a/test-suite/bugs/closed/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.