aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Amin Timany <amintimany@gmail.com>2017-05-02 12:56:14 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-16 04:51:17 +0200
commit4bf85270a36a0a3f9517d8bce92d843f882af00a (patch)
tree5bb66264002d6b1a0cedbf499d49753d3f4905c1 /kernel
parentfece24ec8aa88950477ccfed70b511f05b438718 (diff)
Simplify Univ.ml
Diffstat (limited to 'kernel')
-rw-r--r--kernel/univ.ml4
-rw-r--r--kernel/univ.mli4
2 files changed, 0 insertions, 8 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 5de45cf2b..eb45f022e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1091,10 +1091,6 @@ struct
let (ctx, ctx') = (halve_context (UContext.instance subtypcst))in
Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx'
- let dest x = x
-
- let size ((x,_), _) = Instance.length x
-
end
type universe_info_ind = UInfoInd.t
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