diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-19 20:11:39 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-19 20:11:39 +0000 |
commit | ca05ae9d85000d42fe855bdcf055cfd1dacf15b8 (patch) | |
tree | d64f945378d9d61b8bec704bd1f80c477fde987e | |
parent | 931eb8cc88d61950feb99a05a0936313c53f1688 (diff) |
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
-rw-r--r-- | pretyping/evarutil.ml | 24 |
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 |