Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?n

dans certains cas. Branchement au passage de w_unify vers evar_conv et
solve_simple_eqn en cas d'équations entre Evars.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10623 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 22 insertions, 3 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 890f0bd787..d4cd9d6eaa 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -420,6 +420,12 @@ let order_metas metas =
       else meta :: order latemetas metas
   in order [] metas
 
+(* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
+
+let solve_simple_evar_eqn env evd ev rhs =
+  let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in
+  if b then evd else error_cannot_unify env (evars_of evd) (mkEvar ev,rhs)
+
 (* [w_merge env sigma b metas evars] merges common instances in metas
    or in evars, possibly generating new unification problems; if [b]
    is true, unification of types of metas is required *)
@@ -437,11 +443,10 @@ let w_merge env with_types flags metas evars evd =
 	  w_merge_rec evd (metas'@metas) (evars''@evars') eqns
     	else begin
           let rhs' = subst_meta_instances metas rhs in
-	  if occur_evar evn rhs' then error "w_merge: recursive equation";
           match kind_of_term rhs with
 	  | App (f,cl) when is_mimick_head f ->
 	      (try 
-		  w_merge_rec (evar_define env ev rhs' evd)
+		  w_merge_rec (solve_simple_evar_eqn env evd ev rhs')
                     metas evars' eqns
 		with ex when precatchable_exception ex ->
                   let evd' =
@@ -449,7 +454,8 @@ let w_merge env with_types flags metas evars evd =
 		  w_merge_rec evd' metas evars eqns)
           | _ ->
               (* ensure tail recursion in non-mimickable case! *)
-	      w_merge_rec (evar_define env ev rhs' evd) metas evars' eqns
+	      w_merge_rec (solve_simple_evar_eqn env evd ev rhs') 
+	        metas evars' eqns
 	  end
     | [] -> 
 
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 6a4d928512..e31d67d8cd 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -96,3 +96,16 @@ Goal (forall x, 0 * x = 0 -> True) -> True.
 intros; eapply H.
 rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *)
 Abort.
+
+(* Check handling of identity equation between evars *)
+(* The example failed to pass until revision 10623 *)
+
+Lemma l6 :
+  (forall y, (forall x, (forall z, y = 0 -> y + z = 0) -> y + x = 0) -> True)
+  -> True.
+intros.
+eapply H.
+intros.
+apply H0. (* Check that equation ?n[H] = ?n[H] is correctly considered true *)
+reflexivity.
+Qed.