diff options
| author | Pierre-Marie Pédrot | 2020-04-16 17:06:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-16 17:06:05 +0200 |
| commit | d2d55a710b26e48c94b3241077f30938c1ffb5e8 (patch) | |
| tree | 29bb77fb1a61d54bd0ecfc93e3b937293f9cc641 /vernac/classes.ml | |
| parent | 98eed893760510171e9e8285aac1a8fbeba9afd1 (diff) | |
| parent | 5979601bbb4733d0b9032e918012438f89ada8fe (diff) | |
Merge PR #11982: Fix #11854 error message on unsolved evars in Instance.
Reviewed-by: ppedrot
Diffstat (limited to 'vernac/classes.ml')
| -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 a9425b15d2..eb735b7cdf 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 = |