From a7153b347f8196122394e9ce912055cdf9e575ae Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 28 Apr 2018 19:47:48 +0200
Subject: Move solve_constraint_system near its only use site (comInductive)

---
 engine/universes.ml  | 67 ----------------------------------------------------
 engine/universes.mli |  5 ----
 2 files changed, 72 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index 29c9bd017..01660fe04 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -717,73 +717,6 @@ let refresh_constraints univs (ctx, cstrs) =
       cstrs (Univ.Constraint.empty, univs)
   in ((ctx, cstrs'), univs')
 
-
-(**********************************************************************)
-(* Tools for sort-polymorphic inductive types                         *)
-
-(* Miscellaneous functions to remove or test local univ assumed to
-   occur only in the le constraints *)
-
-(*
-   Solve a system of universe constraint of the form
-
-   u_s11, ..., u_s1p1, w1 <= u1
-   ...
-   u_sn1, ..., u_snpn, wn <= un
-
-where
-
-  - the ui (1 <= i <= n) are universe variables,
-  - the sjk select subsets of the ui for each equations,
-  - the wi are arbitrary complex universes that do not mention the ui.
-*)
-
-let is_direct_sort_constraint s v = match s with
-  | Some u -> univ_level_mem u v
-  | None -> false
-
-let solve_constraints_system levels level_bounds level_min =
-  let open Univ in
-  let levels =
-    Array.mapi (fun i o ->
-      match o with
-      | Some u ->
-	(match Universe.level u with 
-	| Some u -> Some u 
-	| _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
-      | None -> None)
-      levels in
-  let v = Array.copy level_bounds in
-  let nind = Array.length v in
-  let clos = Array.map (fun _ -> Int.Set.empty) levels in
-  (* First compute the transitive closure of the levels dependencies *)
-  for i=0 to nind-1 do
-    for j=0 to nind-1 do
-      if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
-	clos.(i) <- Int.Set.add j clos.(i);
-    done;
-  done;
-  let rec closure () = 
-    let continue = ref false in
-      Array.iteri (fun i deps -> 
-	let deps' = 
-	  Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps
-	in 
-	  if Int.Set.equal deps deps' then ()
-	  else (clos.(i) <- deps'; continue := true))
-	clos;
-      if !continue then closure ()
-      else ()
-  in 
-  closure ();
-  for i=0 to nind-1 do
-    for j=0 to nind-1 do
-      if not (Int.equal i j) && Int.Set.mem j clos.(i) then
-	(v.(i) <- Universe.sup v.(i) level_bounds.(j));
-    done;
-  done;
-  v
-
 (** Deprecated *)
 
 (** UnivNames *)
diff --git a/engine/universes.mli b/engine/universes.mli
index da4a00751..bd315f277 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -124,11 +124,6 @@ val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t
 
 val pr_universe_opt_subst : universe_opt_subst -> Pp.t
 
-(** {6 Support for template polymorphism } *)
-
-val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array ->
-  Universe.t array
-
 (** *********************************** Deprecated *)
 
 [@@@ocaml.warning "-3"]
-- 
cgit v1.2.3