Nouveaux bugs instanciation d'evar par des evar

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

1 files changed, 14 insertions, 10 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d24f8b9c2..3b6acb1ba 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -97,7 +97,7 @@ let split_evar_to_arrow sigma c =
  * What we do is that ?2 is defined by a new evar ?4 whose context will be
  * a prefix of ?2's env, included in ?1's env. *)
 
-let do_restrict_hyps sigma (ev,args) =
+let do_restrict_hyps sigma ev args =
   let args = Array.to_list args in
   let evd = Evd.map sigma ev in
   let env = evar_env evd in
@@ -163,8 +163,7 @@ let ise_defined isevars c = match kind_of_term c with
   | IsEvar (n,_) -> Evd.is_defined !isevars n
   | _ -> false
 
-let need_restriction isevars (n,args) =
-  not (Evd.is_defined !isevars n) & not (array_for_all closed0 args)
+let need_restriction isevars args = not (array_for_all closed0 args)
     
 
 (* We try to instanciate the evar assuming the body won't depend
@@ -182,13 +181,18 @@ let real_clean isevars sp args rhs =
       | IsRel i ->
  	 if i<=k then t
  	 else (try List.assoc (mkRel (i-k)) subst with Not_found -> t)
-      | IsEvar ev ->
-	  if need_restriction isevars ev then begin
-	    let (sigma,rc) = do_restrict_hyps !isevars ev in
-	    isevars := sigma;
-	    rc
-	  end else
-	    t
+      | IsEvar (ev,args) ->
+	  let args' = Array.map (subs k) args in
+	  if need_restriction isevars args' then
+	    if Evd.is_defined !isevars ev then 
+	      subs k (existential_value !isevars (ev,args'))
+	    else begin
+	      let (sigma,rc) = do_restrict_hyps !isevars ev args' in
+	      isevars := sigma;
+	      rc
+	    end
+	  else
+	    mkEvar (ev,args')
       | IsVar _ -> (try List.assoc t subst with Not_found -> t)
       | _ -> map_constr_with_binders succ subs k t
   in