diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 08:11:07 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-22 11:33:57 +0100 |
| commit | 88afd8a9853c772b6b1681c7ae208e55e7daacbe (patch) | |
| tree | 7561c915ee289a94ea29ff5538fbafa004f4e901 /vernac | |
| parent | 23f0f5fe6b510d2ab91a2917eb895faa479d9fcf (diff) | |
[api] Deprecate Term destructors, move to Constr
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 6 | ||||
| -rw-r--r-- | vernac/himsg.ml | 4 | ||||
| -rw-r--r-- | vernac/record.ml | 3 |
3 files changed, 7 insertions, 6 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index fd0027c40..257c003b5 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -8,8 +8,8 @@ open Pp open CErrors +open Sorts open Util -open Term open Constr open Vars open Termops @@ -376,8 +376,8 @@ let rec check_anonymous_type ind = | _ -> false let make_conclusion_flexible evdref ty poly = - if poly && isArity ty then - let _, concl = destArity ty in + if poly && Term.isArity ty then + let _, concl = Term.destArity ty in match concl with | Type u -> (match Univ.universe_level u with diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 839064aa0..e8c5aeedd 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -11,7 +11,7 @@ open Util open Names open Nameops open Namegen -open Term +open Constr open Termops open Indtypes open Environ @@ -405,7 +405,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 Term.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." + (if Constr.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." (* TODO: use the names *) (* (co)fixpoints *) diff --git a/vernac/record.ml b/vernac/record.ml index 1bd47a556..f09b57048 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -8,11 +8,12 @@ open Pp open CErrors +open Term +open Sorts open Util open Names open Globnames open Nameops -open Term open Constr open Vars open Environ |