diff options
| -rw-r--r-- | pretyping/evarutil.ml | 6 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 |
2 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 1d5df55f3e..23f5a74c80 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -336,8 +336,10 @@ let evar_define env (ev,argsv) rhs isevars = (* the bindings to invert *) let worklist = make_subst (evar_env evi) args in let (isevars',body) = real_clean env isevars ev worklist rhs in - let isevars'' = Evd.evar_define ev body isevars' in - isevars'',[ev] + if occur_meta body then error "Meta cannot occur in evar body" + else + let isevars'' = Evd.evar_define ev body isevars' in + isevars'',[ev] (* [w_Define evd sp c] (tactic style) * diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b5e175dd82..2801d3ee49 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -224,14 +224,14 @@ let w_merge env with_types mod_delta metas evars evd = match krhs with | App (f,cl) when is_mimick_head f -> (try - w_merge_rec (w_Define evn rhs' evd) metas t + w_merge_rec (fst (evar_define env ev rhs' evd)) metas t with ex when precatchable_exception ex -> let evd' = mimick_evar evd mod_delta f (Array.length cl) evn in w_merge_rec evd' metas evars) | _ -> (* ensure tail recursion in non-mimickable case! *) - w_merge_rec (w_Define evn rhs' evd) metas t + w_merge_rec (fst (evar_define env ev rhs' evd)) metas t end | _ -> anomaly "w_merge_rec")) |