diff options
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 96be6c14a..3aaad5877 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 |