diff options
Diffstat (limited to 'vernac')
| -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 () ++ |