diff options
| author | Hugo Herbelin | 2014-11-03 20:02:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-03 20:43:16 +0100 |
| commit | 9a6e94199b4df828f160e4a107debd7cb16e66bc (patch) | |
| tree | af0316b9841ed92c173be075fae39921bb9893cd | |
| parent | 71c56620314bc28c6d7a643a2174518e74da6d50 (diff) | |
Now that evars can be parsed, protect strongly Check from calling kernel with evars.
| -rw-r--r-- | toplevel/vernacentries.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index ab5cee5cde..34538f21fd 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1490,11 +1490,11 @@ let vernac_check_may_eval redexp glopt rc = let env = Environ.push_context uctx env in let c = nf c in let j = - try - Evarutil.check_evars env sigma sigma' c; - Arguments_renaming.rename_typing env c - with Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) -> - Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in + if Evarutil.has_undefined_evars sigma' c then + Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) + else + (* OK to call kernel which does not support evars *) + Arguments_renaming.rename_typing env c in match redexp with | None -> let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in |