diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ca77e03707..ad6ca3a84e 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -391,11 +391,10 @@ let explain_unexpected_type env sigma actual_type expected_type = str "where" ++ spc () ++ prexp ++ str " was expected." let explain_not_product env sigma c = - let c = EConstr.to_constr sigma c in - let pr = pr_lconstr_env env sigma c in + let pr = pr_econstr_env env sigma c in str "The type of this term is a product" ++ spc () ++ str "while it is expected to be" ++ - (if Constr.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." + (if EConstr.isType sigma c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." (* TODO: use the names *) (* (co)fixpoints *) @@ -769,7 +768,7 @@ let pr_constraints printenv env sigma evars cstrs = h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs) else let filter evk _ = Evar.Map.mem evk evars in - pr_evar_map_filter ~with_univs:false filter sigma + pr_evar_map_filter ~with_univs:false filter env sigma let explain_unsatisfiable_constraints env sigma constr comp = let (_, constraints) = Evd.extract_all_conv_pbs sigma in |