diff options
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 e15911dd6..12b68fe38 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -418,7 +418,7 @@ let explain_not_product env sigma c = let pr = pr_lconstr_env env sigma c in str "The type of this term is a product" ++ spc () ++ str "while it is expected to be" ++ - (if is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." + (if Term.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." (* TODO: use the names *) (* (co)fixpoints *) |