diff options
| author | Emilio Jesus Gallego Arias | 2017-11-06 23:27:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-06 23:46:52 +0100 |
| commit | 03e21974a3e971a294533bffb81877dc1bd270b6 (patch) | |
| tree | 1b37339378f6bc93288b61f707efb6b08f992dc5 /kernel/typeops.mli | |
| parent | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff) | |
[api] Move structures deprecated in the API to the core.
We do up to `Term` which is the main bulk of the changes.
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 96be6c14a4..3aaad5877b 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -8,7 +8,7 @@ open Names open Univ -open Term +open Constr open Environ open Entries @@ -41,8 +41,8 @@ val type1 : types val type_of_sort : Sorts.t -> types val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment -val judge_of_prop_contents : contents -> unsafe_judgment -val judge_of_type : universe -> unsafe_judgment +val judge_of_prop_contents : Sorts.contents -> unsafe_judgment +val judge_of_type : Universe.t -> unsafe_judgment (** {6 Type of a bound variable. } *) val type_of_relative : env -> int -> types @@ -71,8 +71,8 @@ val judge_of_abstraction : -> unsafe_judgment (** {6 Type of a product. } *) -val sort_of_product : env -> sorts -> sorts -> sorts -val type_of_product : env -> Name.t -> sorts -> sorts -> types +val sort_of_product : env -> Sorts.t -> Sorts.t -> Sorts.t +val type_of_product : env -> Name.t -> Sorts.t -> Sorts.t -> types val judge_of_product : env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment |