diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 17:26:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-17 18:46:09 +0200 |
| commit | aa5e962c9888889380ae85a7cbd82a8ac4779a0f (patch) | |
| tree | 6086365bd58c072e22efb4c5e57133338ed2d991 /engine/universes.mli | |
| parent | 5281317cb558f2b9aa6f854b9c7aeb617beba8e6 (diff) | |
Make set minimization option internal to Universes
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 |