diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:38:45 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:38:45 +0200 |
| commit | d6d7a12eb49c997dd83298477e216349fad74c7f (patch) | |
| tree | aa4648227f0b1a5c5e9c1b5e6e2f17818db73413 /vernac/himsg.ml | |
| parent | d2406149554812a01ac615af43af6b7b2a3efd72 (diff) | |
| parent | a1efd8080465eb49b30b5bab61cf3861899876e4 (diff) | |
Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.
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 *) |