2 files changed, 40 insertions, 6 deletions
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index e83e7176d..c70467912 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 000000000..874abf49f
--- /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).