diff options
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 546f2d2b4..3b2abc777 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -43,7 +43,6 @@ 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 : Sorts.contents -> unsafe_judgment val judge_of_type : Universe.t -> unsafe_judgment (** {6 Type of a bound variable. } *) |