Add tolerance for existential variables in Check.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13599 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 6 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7797db4730..5962cf14d4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1028,18 +1028,25 @@ let get_current_context_of_args = function
   | None -> get_current_context ()
 
 let vernac_check_may_eval redexp glopt rc =
-  let (evmap,env) = get_current_context_of_args glopt in
-  let c = interp_constr evmap env rc in
-  let j = Typeops.typing env c in
+  let module P = Pretype_errors in
+  let (sigma, env) = get_current_context_of_args glopt in
+  let j =
+    let sigma', c = interp_open_constr sigma env rc in
+    try
+      Evarutil.check_evars env sigma sigma' c;
+      Typeops.typing env c
+    with P.PretypeError (_,P.UnsolvableImplicit _)
+      | Compat.Loc.Exc_located (_,P.PretypeError (_,P.UnsolvableImplicit _)) ->
+      Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in
   match redexp with
     | None ->
 	if !pcoq <> None then (Option.get !pcoq).print_check env j
 	else msg (print_judgment env j)
     | Some r ->
-	let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in
+	let redfun = fst (reduction_of_red_expr (interp_redexp env sigma r)) in
 	if !pcoq <> None
-	then (Option.get !pcoq).print_eval redfun env evmap rc j
-	else msg (print_eval redfun env evmap rc j)
+	then (Option.get !pcoq).print_eval redfun env sigma rc j
+	else msg (print_eval redfun env sigma rc j)
 
 let vernac_declare_reduction locality s r =
   declare_red_expr locality s (interp_redexp (Global.env()) Evd.empty r)