From f53890d1629ea7aaff86ea92e5ac27ab027b2e8d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Mar 2018 13:37:07 +0100 Subject: universe normalisation: put equivalence class partition in UGraph ie don't go through having Eq constraints but directly to the unionfind. --- engine/universes.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'engine/universes.mli') diff --git a/engine/universes.mli b/engine/universes.mli index 4823c5746..a0a7749f8 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -162,8 +162,6 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t -> (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -module UF : Unionfind.PartitionSig with type elt = Level.t - val level_subst_of : universe_subst_fn -> universe_level_subst_fn val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t -- cgit v1.2.3