diff options
| author | Pierre-Marie Pédrot | 2020-05-12 12:02:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-12 12:07:43 +0200 |
| commit | d31cb4d3e55da99d42abdc1f4129ddc03e1631c6 (patch) | |
| tree | fa0648deb47650cc0d026ecdd711c093d36e585c /vernac/himsg.ml | |
| parent | e802f48faf7a472000e218c7a3321c10c2171e0f (diff) | |
Do not use Unsafe.to_constr for old refiner conclusion.
This was useless, since we did not observe the difference on evars.
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 41f2ab9c63..4fe3f07d6e 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1096,7 +1096,7 @@ let explain_typeclass_error env sigma = function (* Refiner errors *) let explain_refiner_bad_type env sigma arg ty conclty = - let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_lconstr_env env sigma conclty) in + let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_leconstr_env env sigma conclty) in str "Refiner was given an argument" ++ brk(1,1) ++ pr_lconstr_env env sigma arg ++ spc () ++ str "of type" ++ brk(1,1) ++ pm ++ spc () ++ |