From 75d51735e95d43323b03ecf586c6aba163cf70a6 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 20 Mar 2012 08:02:18 +0000
Subject: 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
---
 toplevel/vernacentries.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'toplevel')

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;
-- 
cgit v1.2.3