From 5dba392f32f0da65a4f0331186e75b35fffa1bb7 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 22 Feb 2010 01:40:01 +0000
Subject: Improve unification when evars and metas are mixed. If we can't
 mimick a rhs in an ?evar = rhs situation, we first turn all metas in rhs into
 evars before trying to solve the equation. Problem reported by Eelis van der
 Weegen.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12801 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/unification.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d26195efc8..32b51eac49 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -637,11 +637,16 @@ let w_merge env with_types flags (evd,metas,evars) =
     	else begin
           let rhs' = subst_meta_instances metas rhs in
           match kind_of_term rhs with
-	  | App (f,cl) when is_mimick_head f & occur_meta rhs' ->
+	  | App (f,cl) when occur_meta rhs' ->
 	      if occur_evar evn rhs' then
                 error_occur_check env evd evn rhs';
-	      let evd' = mimick_evar evd flags f (Array.length cl) evn in
-	      w_merge_rec evd' metas evars eqns
+	      if is_mimick_head f then
+		let evd' = mimick_evar evd flags f (Array.length cl) evn in
+		  w_merge_rec evd' metas evars eqns
+	      else
+		let evd', rhs'' = pose_all_metas_as_evars env evd rhs' in
+	  	  w_merge_rec (solve_simple_evar_eqn env evd' ev rhs'')
+		    metas evars' eqns
           | _ ->
 	      w_merge_rec (solve_simple_evar_eqn env evd ev rhs')
 		metas evars' eqns
-- 
cgit v1.2.3