diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-09-12 16:37:43 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-09-12 16:37:43 +0200 |
| commit | a1efd8080465eb49b30b5bab61cf3861899876e4 (patch) | |
| tree | 2a84202fc27b668288f3e9b6a6b6773b79522447 /vernac/himsg.ml | |
| parent | cc94172036789cfef28007f59510b7f17df5d45d (diff) | |
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 2be10a039..b8f0c4099 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 *) |