From 302adae094bbf76d8c951c557c85acb12a97aedc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 28 Apr 2018 21:27:15 +0200
Subject: Split off Universes functions about substitutions and constraints

---
 pretyping/unification.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'pretyping/unification.ml')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f9a22b065..62bee5a36 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -561,16 +561,16 @@ let is_rigid_head sigma flags t =
     | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
 
 let force_eqs c =
-  let open Universes in
-  Constraints.fold
+  let open UnivProblem in
+  Set.fold
     (fun c acc ->
        let c' = match c with
          (* Should we be forcing weak constraints? *)
          | ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r)
          | ULe _ | UEq _ -> c
        in
-        Constraints.add c' acc)
-    c Constraints.empty
+        Set.add c' acc)
+    c Set.empty
 
 let constr_cmp pb env sigma flags t u =
   let cstrs =
-- 
cgit v1.2.3