aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/univ.mli')
-rw-r--r--checker/univ.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/checker/univ.mli b/checker/univ.mli
index 6cd3b3638..3b29b158f 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -109,8 +109,6 @@ type 'a constrained = 'a * constraints
type 'a constraint_function = 'a -> 'a -> constraints -> constraints
-val enforce_leq : universe constraint_function
-
(** {6 ... } *)
(** Merge of constraints in a universes graph.
The function [merge_constraints] merges a set of constraints in a given