diff options
Diffstat (limited to 'engine/universes.mli')
| -rw-r--r-- | engine/universes.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index df2e961d6..46d65f257 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -17,9 +17,6 @@ open Univ (** Unordered pairs of universe levels (ie (u,v) = (v,u)) *) module UPairSet : CSet.S with type elt = (Level.t * Level.t) -val set_minimization : bool ref -val is_set_minimization : unit -> bool - (** Universes *) val pr_with_global_universes : Level.t -> Pp.t |