aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/univ.mli')
-rw-r--r--kernel/univ.mli4
1 files changed, 0 insertions, 4 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 114193329..53af80448 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -336,8 +336,6 @@ sig
val univ_context : t -> universe_context
val subtyp_context : t -> universe_context
- val dest : t -> universe_context * universe_context
-
(** This function takes a universe context representing constraints
of an inductive and a Instance.t of fresh universe names for the
subtyping (with the same length as the context in the given
@@ -347,8 +345,6 @@ sig
val subtyping_susbst : t -> universe_level_subst
- val size : t -> int
-
end
type universe_info_ind = UInfoInd.t