From 5979601bbb4733d0b9032e918012438f89ada8fe Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Mar 2020 15:57:25 +0200
Subject: Fix #11854 error message on unsolved evars in Instance.

---
 vernac/classes.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3d38713e09..a411300b54 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -485,10 +485,8 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp
     interp_props ~program_mode:false env' cty k u ctx ctx' subst sigma props
   in
   let termtype, sigma = do_instance_resolve_TC termtype sigma env in
-  if Evd.has_undefined sigma then
-    CErrors.user_err Pp.(str "Unsolved obligations remaining.")
-  else
-    declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
+  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
+  declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
 
 let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
   let term, termtype, sigma =
-- 
cgit v1.2.3