From 9a6e94199b4df828f160e4a107debd7cb16e66bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 3 Nov 2014 20:02:44 +0100
Subject: Now that evars can be parsed, protect strongly Check from calling
 kernel with evars.

---
 toplevel/vernacentries.ml | 10 +++++-----
 1 file 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
-- 
cgit v1.2.3