Merge PR#379: Introducing evar-insensitive constrs

4 files changed, 61 insertions, 6 deletions

diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index e83e7176de..c70467912f 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,13 +6,13 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x : T n := A n in ?y ?y0 : T n
+fun n : nat => let x : T n := A n in ?t ?y : T n
      : forall n : nat, T n
 where
-?y : [n : nat  x := A n : T n |- ?T -> T n] 
-?y0 : [n : nat  x := A n : T n |- ?T] 
-fun n : nat => ?y ?y0 : T n
+?t : [n : nat  x := A n : T n |- ?T -> T n] 
+?y : [n : nat  x := A n : T n |- ?T] 
+fun n : nat => ?t ?y : T n
      : forall n : nat, T n
 where
-?y : [n : nat |- ?T -> T n] 
-?y0 : [n : nat |- ?T] 
+?t : [n : nat |- ?T -> T n] 
+?y : [n : nat |- ?T] 
diff --git a/test-suite/success/change_pattern.v b/test-suite/success/change_pattern.v
new file mode 100644
index 0000000000..874abf49f1
--- /dev/null
+++ b/test-suite/success/change_pattern.v
@@ -0,0 +1,34 @@
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Axiom vector : Type -> nat -> Type.
+
+Record KleeneStore i j a := kleeneStore
+ { dim : nat
+ ; peek : vector j dim -> a
+ ; pos : vector i dim
+ }.
+
+Definition KSmap i j a b (f : a -> b) (s : KleeneStore i j a) : KleeneStore i j b :=
+  kleeneStore (fun v => f (peek v)) (pos s).
+
+Record KleeneCoalg (i o : Type -> Type) := kleeneCoalg
+  { coalg :> forall a b, (o a) -> KleeneStore (i a) (i b) (o b) }.
+
+Axiom free_b_dim : forall i o (k : KleeneCoalg i o) a b b' (x : o a), dim (coalg k b x) = dim (coalg k b' x).
+Axiom t : Type -> Type.
+Axiom traverse : KleeneCoalg (fun x => x) t.
+
+Definition size a (x:t a) : nat := dim (traverse a a x).
+
+Lemma iso1_iso2_2 a (y : {x : t unit & vector a (size x)}) : False.
+Proof.
+destruct y.
+pose (X := KSmap (traverse a unit) (traverse unit a x)).
+set (e :=(eq_sym (free_b_dim traverse (a:=unit) a unit x))).
+clearbody e.
+(** The pattern generated by change must have holes where there were implicit
+    arguments in the original user-provided term. This particular example fails
+    if this is not the case because the inferred argument does not coincide with
+    the one in the considered term. *)
+progress (change (dim (traverse unit a x)) with (dim X) in e).
diff --git a/test-suite/success/old_typeclass.v b/test-suite/success/old_typeclass.v
new file mode 100644
index 0000000000..01e35810b0
--- /dev/null
+++ b/test-suite/success/old_typeclass.v
@@ -0,0 +1,13 @@
+Require Import Setoid Coq.Classes.Morphisms.
+Set Typeclasses Legacy Resolution.
+
+Declare Instance and_Proper_eq: Proper (Logic.eq ==> Logic.eq ==> Logic.eq) and.
+
+Axiom In : Prop.
+Axiom union_spec : In <-> True.
+
+Lemma foo : In /\ True.
+Proof.
+progress rewrite union_spec.
+repeat constructor.
+Qed.
diff --git a/test-suite/success/rewrite_evar.v b/test-suite/success/rewrite_evar.v
new file mode 100644
index 0000000000..f7ad261cbb
--- /dev/null
+++ b/test-suite/success/rewrite_evar.v
@@ -0,0 +1,8 @@
+Require Import Coq.Setoids.Setoid.
+
+Goal forall (T2 MT1 MT2 : Type) (x : T2) (M2 m2 : MT2) (M1 m1 : MT1) (F : T2 -> MT1 -> MT2 -> Prop),
+    (forall (defaultB : T2) (m3 : MT1) (m4 : MT2), F defaultB m3 m4 <-> True) -> F x M1 M2 -> F x m1 m2.
+  intros ????????? H' H.
+  rewrite (H' _) in *.
+  (** The above rewrite should also rewrite in H. *)
+  Fail progress rewrite H' in H.