diff options
| author | barras | 2004-09-08 13:53:52 +0000 |
|---|---|---|
| committer | barras | 2004-09-08 13:53:52 +0000 |
| commit | 2cc7db038d72006bf7d3b418df450c370e447421 (patch) | |
| tree | 2942b639ef6085cb7d2740c78b5d6e4aa36b9685 | |
| parent | dee2a3d461eddffa1e858bb4a0af92dfa7575d81 (diff) | |
petit bug avec les effets de bords
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6078 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarutil.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index aa079e7ceb..58b3f3ac2f 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -278,16 +278,14 @@ let real_clean env isevars ev args rhs = else (try List.assoc (mkRel (i-k)) subst with Not_found -> t) | Evar (ev,args) -> let args' = Array.map (subs k) args in - if need_restriction isevars args' then - if Evd.is_defined isevars.evars ev then - subs k (existential_value isevars.evars (ev,args')) - else begin - let (sigma,rc) = do_restrict_hyps isevars.evars ev args' in + if need_restriction !evd args' then + begin + let (sigma,rc) = do_restrict_hyps !evd.evars ev args' in evd := {!evd with evars = sigma; history = - (fst (destEvar rc),evar_source ev isevars):: !evd.history}; + (fst (destEvar rc),evar_source ev !evd):: !evd.history}; rc end else @@ -297,7 +295,7 @@ let real_clean env isevars ev args rhs = in let body = subs 0 rhs in if not (closed0 body) - then error_not_clean env isevars.evars ev body (evar_source ev isevars); + then error_not_clean env !evd.evars ev body (evar_source ev !evd); (!evd,body) let make_evar_instance_with_rel env = @@ -505,8 +503,7 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 = let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) = let t2 = nf_evar isevars.evars t2 in let (isevars,lsp) = match kind_of_term t2 with - | Evar (n2,args2 as ev2) - when not (Evd.is_defined isevars.evars n2) -> + | Evar (n2,args2 as ev2) -> if n1 = n2 then solve_refl conv_algo env isevars n1 args1 args2 else |