Fix canonical structure resolution in unification (bug found in Ssreflect).

2 files changed, 23 insertions, 14 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 5265a875b0..7df4dabcd4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -126,7 +126,7 @@ let check_conv_record (t1,sk1) (t2,sk2) =
 	  lookup_canonical_conversion (proji, Const_cs c2),sk2
     with Not_found ->
       let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in 
-	(t2,cs),[]
+	(c,cs),[]
   in
   let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
         o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
@@ -687,8 +687,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),
     in
     let app = mkApp (c, Array.rev_of_list ks) in
     ise_and evd'
-      [test;
-       (fun i ->
+      [(fun i ->
 	exact_ise_stack2 env i
           (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x))
           params1 params);
@@ -698,7 +697,9 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),
            us2 us);
        (fun i -> evar_conv_x trs env i CONV c1 app);
        (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1);
-       (fun i -> evar_conv_x trs env i CONV h (substl ks h'))]
+       test;
+       (fun i -> evar_conv_x trs env i CONV h 
+	 (fst (decompose_app_vect (substl ks h'))))]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
 and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) =
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
index 97cf316cad..d819dc47aa 100644
--- a/test-suite/success/AdvancedCanonicalStructure.v
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -47,6 +47,24 @@ Goal forall a1 a2, eqA (plusA a1 zeroA) a2.
 change (eqB (plusB (phi a1) zeroB) (phi a2)).
 Admitted.
 
+Variable foo : A -> Type.
+
+Definition local0 := fun (a1 : A) (a2 : A) (a3 : A) =>
+                       (eq_refl : plusA a1 (plusA zeroA a2) = ia _).
+Definition local1 := 
+  fun (a1 : A) (a2 : A) (f : A -> A) => 
+    (eq_refl : plusA a1 (plusA zeroA (f a2)) = ia _).
+
+Definition local2 := 
+  fun (a1 : A) (f : A -> A) => 
+    (eq_refl : (f a1) = ia _).
+
+Goal forall a1 a2, eqA (plusA a1 zeroA) a2.
+  intros a1 a2.
+  refine  (eq_img _ _  _).
+change (eqB (plusB (phi a1) zeroB) (phi a2)).
+Admitted.
+
 End group_morphism.
 
 Open Scope type_scope.
@@ -129,13 +147,3 @@ Admitted.
 Check L : abs _ .
 
 End type_reification.
-
-
-
-
-
-
-
-
-
-