From d41eaff0b2c6f2ff10ef851864abfa3366862d22 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 28 Apr 2018 21:30:59 +0200
Subject: Make Universes.refresh_constraints internal to UState

---
 engine/uState.ml     | 21 ++++++++++++++++++++-
 engine/universes.ml  | 18 ------------------
 engine/universes.mli |  2 --
 3 files changed, 20 insertions(+), 21 deletions(-)

(limited to 'engine')

diff --git a/engine/uState.ml b/engine/uState.ml
index 6111ec7ed..dbf5d48aa 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -553,12 +553,31 @@ let is_sort_variable uctx s =
 let subst_univs_context_with_def def usubst (ctx, cst) =
   (Univ.LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst)
 
+let is_trivial_leq (l,d,r) =
+  Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))
+
+(* Prop < i <-> Set+1 <= i <-> Set < i *)
+let translate_cstr (l,d,r as cstr) =
+  let open Univ in
+  if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then
+    (Level.set, d, r)
+  else cstr
+
+let refresh_constraints univs (ctx, cstrs) =
+  let cstrs', univs' =
+    Univ.Constraint.fold (fun c (cstrs', univs as acc) ->
+      let c = translate_cstr c in
+      if is_trivial_leq c then acc
+      else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs))
+      cstrs (Univ.Constraint.empty, univs)
+  in ((ctx, cstrs'), univs')
+
 let normalize_variables uctx =
   let normalized_variables, undef, def, subst = 
     UnivSubst.normalize_univ_variables uctx.uctx_univ_variables
   in
   let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
-  let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in
+  let ctx_local', univs = refresh_constraints uctx.uctx_initial_universes ctx_local in
     subst, { uctx with uctx_local = ctx_local';
       uctx_univ_variables = normalized_variables;
       uctx_universes = univs }
diff --git a/engine/universes.ml b/engine/universes.ml
index 009328571..e3b661770 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -384,24 +384,6 @@ let normalize_context_set g ctx us algs weak =
 (* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
 (* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
 
-let is_trivial_leq (l,d,r) =
-  Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))
-
-(* Prop < i <-> Set+1 <= i <-> Set < i *)
-let translate_cstr (l,d,r as cstr) =
-  if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then
-    (Level.set, d, r)
-  else cstr
-
-let refresh_constraints univs (ctx, cstrs) =
-  let cstrs', univs' = 
-    Univ.Constraint.fold (fun c (cstrs', univs as acc) -> 
-      let c = translate_cstr c in
-      if is_trivial_leq c then acc
-      else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs))
-      cstrs (Univ.Constraint.empty, univs)
-  in ((ctx, cstrs'), univs')
-
 (** Deprecated *)
 
 (** UnivNames *)
diff --git a/engine/universes.mli b/engine/universes.mli
index 3e397ed57..4d7105e72 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -36,8 +36,6 @@ val normalize_context_set : UGraph.t -> ContextSet.t ->
   UPairSet.t (* weak equality constraints *) ->
   (universe_opt_subst * LSet.t) in_universe_context_set
 
-val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t
-
 (** *********************************** Deprecated *)
 
 [@@@ocaml.warning "-3"]
-- 
cgit v1.2.3