diff options
| author | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
| commit | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch) | |
| tree | 675b02e411ff2c56a9aff39f4956a055eac254a7 /kernel/typeops.mli | |
| parent | 29a7307ea7cd36408661ba633a235793f11dca84 (diff) | |
| parent | 03e21974a3e971a294533bffb81877dc1bd270b6 (diff) | |
Merge PR #6098: [api] Move structures deprecated in the API to the core.
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 |