Force Check (which, from 8.4beta, accepts unresolved evars) to however

try to solve remaining constraints.

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

1 files changed, 1 insertions, 0 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c727cc918..22c89cee6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1183,6 +1183,7 @@ let vernac_check_may_eval redexp glopt rc =
   let module P = Pretype_errors in
   let (sigma, env) = get_current_context_of_args glopt in
   let sigma', c = interp_open_constr sigma env rc in
+  let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in
   let j =
     try
       Evarutil.check_evars env sigma sigma' c;