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

1 files changed, 9 insertions, 3 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 890f0bd78..d4cd9d6ea 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
     | [] ->