diff options
| author | barras | 2004-09-06 15:59:53 +0000 |
|---|---|---|
| committer | barras | 2004-09-06 15:59:53 +0000 |
| commit | 2a405677a527d71c403a173615bd9e2a0cd9c90b (patch) | |
| tree | 806efb125558034df60a7b1bc2ebe3705313d9bc | |
| parent | cc746ea32b1dd61dff9c82db68f2f8ef2131af3f (diff) | |
bad env in mimick code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6065 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/unification.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 359484997b..ecb3b58d73 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -213,7 +213,9 @@ let is_mimick_head f = (Const _|Var _|Rel _|Construct _|Ind _) -> true | _ -> false -let mimick_evar env hdc nargs sp evd = +let mimick_evar hdc nargs sp evd = + let ev = Evd.map (evars_of evd) sp in + let env = Global.env_of_context ev.evar_hyps in let (sigma',c) = applyHead env (evars_of evd) nargs hdc in evars_reset_evd sigma' evd; w_Define sp c evd @@ -257,7 +259,7 @@ let w_merge env with_types metas evars (sigma,metamap) = w_Define evn rhs' evd; w_merge_rec metas t with ex when precatchable_exception ex -> - mimick_evar env f (Array.length cl) evn evd; + mimick_evar f (Array.length cl) evn evd; w_merge_rec metas evars) | _ -> (* ensure tail recursion in non-mimickable case! *) |