diff options
| author | Gaëtan Gilbert | 2020-03-31 15:57:25 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 16:00:28 +0200 |
| commit | 5979601bbb4733d0b9032e918012438f89ada8fe (patch) | |
| tree | 59684d58593739fb56d71d4f4d4e70db0ef9e0b1 | |
| parent | 0beca74bc90cef03d779a8e4f8668335c9c37716 (diff) | |
Fix #11854 error message on unsolved evars in Instance.
| -rw-r--r-- | vernac/classes.ml | 6 |
1 files 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 = |