Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Universes.

Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.

7 files changed, 30 insertions, 30 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 7df4dabcd..8c4ca1d82 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -369,10 +369,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     else evar_eqappr_x ts env' evd CONV out2 out1
   in
   let rigids env evd sk term sk' term' =
-    let b,univs = eq_constr_universes term term' in
+    let b,univs = Universes.eq_constr_universes term term' in
       if b then
 	ise_and evd [(fun i -> 
-	  let cstrs = Univ.to_constraints (Evd.universes i) univs in
+	  let cstrs = Universes.to_constraints (Evd.universes i) univs in
 	    try let i = Evd.add_constraints i cstrs in
 		  Success i
 	    with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
@@ -485,7 +485,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	     allow this identification (first-order unification of universes). Otherwise
 	     fallback to unfolding.
 	  *)
-	  let b,univs = eq_constr_universes term1 term2 in
+	  let b,univs = Universes.eq_constr_universes term1 term2 in
 	    if b then
 	      ise_and i [(fun i -> 
 		try Success (Evd.add_universe_constraints i univs)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index e125a1c6e..adcc7bf38 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -393,7 +393,7 @@ let process_universe_constraints univs vars alg templ cstrs =
 	  | None -> Inl x
 	  | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg)
 	in
-	  if d == Univ.ULe then
+	  if d == Universes.ULe then
 	    if Univ.check_leq univs l r then
 	      (** Keep Prop/Set <= var around if var might be instantiated by prop or set
 		  later. *)
@@ -415,19 +415,19 @@ let process_universe_constraints univs vars alg templ cstrs =
 		      else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, [])))
 		      levels local
 		else if Univ.LSet.mem rl templ && Univ.Universe.is_level l then
-		  unify_universes fo l Univ.UEq r local
+		  unify_universes fo l Universes.UEq r local
 		else
 		  Univ.enforce_leq l r local
-	  else if d == Univ.ULub then
+	  else if d == Universes.ULub then
 	    match varinfo l, varinfo r with
 	    | (Inr (l, true, _), Inr (r, _, _)) 
 	    | (Inr (r, _, _), Inr (l, true, _)) -> 
 	      instantiate_variable l (Univ.Universe.make r) vars; 
 	      Univ.enforce_eq_level l r local
 	    | Inr (_, _, _), Inr (_, _, _) ->
-	      unify_universes true l Univ.UEq r local
+	      unify_universes true l Universes.UEq r local
 	    | _, _ -> assert false
-	  else (* d = Univ.UEq *)
+	  else (* d = Universes.UEq *)
 	    match varinfo l, varinfo r with
 	    | Inr (l', lloc, _), Inr (r', rloc, _) ->
 	      let () = 
@@ -450,7 +450,7 @@ let process_universe_constraints univs vars alg templ cstrs =
 	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, []))
   in
   let local = 
-    Univ.UniverseConstraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
+    Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
       cstrs Univ.Constraint.empty
   in
     !vars, local
@@ -460,10 +460,10 @@ let add_constraints_context ctx cstrs =
   let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> 
     let l = Univ.Universe.make l and r = Univ.Universe.make r in
     let cstr' = 
-      if d == Univ.Lt then (Univ.Universe.super l, Univ.ULe, r)
-      else (l, (if d == Univ.Le then Univ.ULe else Univ.UEq), r)
-    in Univ.UniverseConstraints.add cstr' acc)
-    cstrs Univ.UniverseConstraints.empty
+      if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r)
+      else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r)
+    in Universes.Constraints.add cstr' acc)
+    cstrs Universes.Constraints.empty
   in
   let vars, local' =
     process_universe_constraints ctx.uctx_universes
@@ -1135,7 +1135,7 @@ let set_eq_sort d s1 s2 =
   match is_eq_sort s1 s2 with
   | None -> d
   | Some (u1, u2) -> add_universe_constraints d 
-    (Univ.UniverseConstraints.singleton (u1,Univ.UEq,u2))
+    (Universes.Constraints.singleton (u1,Universes.UEq,u2))
 
 let has_lub evd u1 u2 =
   (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *)
@@ -1143,7 +1143,7 @@ let has_lub evd u1 u2 =
   (* let u1 = normalize u1 and u2 = normalize u2 in *)
     if Univ.Universe.equal u1 u2 then evd
     else add_universe_constraints evd
-      (Univ.UniverseConstraints.singleton (u1,Univ.ULub,u2))
+      (Universes.Constraints.singleton (u1,Universes.ULub,u2))
 
 let set_eq_level d u1 u2 =
   add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty)
@@ -1153,7 +1153,7 @@ let set_leq_level d u1 u2 =
 
 let set_eq_instances ?(flex=false) d u1 u2 =
   add_universe_constraints d
-    (Univ.enforce_eq_instances_univs flex u1 u2 Univ.UniverseConstraints.empty)
+    (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty)
 
 let set_leq_sort evd s1 s2 =
   let s1 = normalize_sort evd s1 
@@ -1167,7 +1167,7 @@ let set_leq_sort evd s1 s2 =
     (* else if Univ.is_type0m_univ u2 then  *)
     (*   raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
     (* else  *)
-      add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2))
+      add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
 	    
 let check_eq evd s s' =
   Univ.check_eq evd.universes.uctx_universes s s'
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 8bdfccb6b..3b58910e1 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -265,7 +265,7 @@ val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
 
 exception UniversesDiffer
 
-val add_universe_constraints : evar_map -> Univ.universe_constraints -> evar_map
+val add_universe_constraints : evar_map -> Universes.universe_constraints -> evar_map
 (** Add the given universe unification constraints to the evar map.
     @raises UniversesDiffer in case a first-order unification fails.
     @raises UniverseInconsistency
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f75da1383..74f14aa14 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -630,8 +630,8 @@ let magicaly_constant_of_fixbody env bd = function
       match constant_opt_value env (cst,u) with
       | None -> bd
       | Some (t,cstrs) -> 
-        let b, csts = eq_constr_universes t bd in
-	let subst = UniverseConstraints.fold (fun (l,d,r) acc -> 
+        let b, csts = Universes.eq_constr_universes t bd in
+	let subst = Universes.Constraints.fold (fun (l,d,r) acc -> 
 	  Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc)
 	  csts Univ.LMap.empty
 	in
@@ -1170,9 +1170,9 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
     let b, sigma = 
       let b, cstrs = 
 	if pb == Reduction.CUMUL then 
-	  Constr.leq_constr_univs_infer (Evd.universes sigma) x y 
+	  Universes.leq_constr_univs_infer (Evd.universes sigma) x y 
 	else
-	  Constr.eq_constr_univs_infer (Evd.universes sigma) x y 
+	  Universes.eq_constr_univs_infer (Evd.universes sigma) x y 
       in
 	if b then 
 	  try true, Evd.add_universe_constraints sigma cstrs
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 8b2532a5f..93e1060ab 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1058,7 +1058,7 @@ let compute = cbv_betadeltaiota
 
 let make_eq_univs_test evd c =
   { match_fun = (fun evd c' -> 
-    let b, cst = eq_constr_universes c c' in 
+    let b, cst = Universes.eq_constr_universes c c' in 
       if b then 
 	try Evd.add_universe_constraints evd cst
 	with Evd.UniversesDiffer -> raise NotUnifiable
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index d728f1bff..363292ec0 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -559,7 +559,7 @@ let collect_vars c =
    [m] is appropriately lifted through abstractions of [t] *)
 
 let dependent_main noevar univs m t =
-  let eqc x y = if univs then fst (eq_constr_universes x y) else eq_constr_nounivs x y in
+  let eqc x y = if univs then fst (Universes.eq_constr_universes x y) else eq_constr_nounivs x y in
   let rec deprec m t =
     if eqc m t then
       raise Occur
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4936ba426..574088f42 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -391,16 +391,16 @@ let is_rigid_head flags t =
   | _ -> false
 
 let force_eqs c = 
-  Univ.UniverseConstraints.fold
+  Universes.Constraints.fold
     (fun ((l,d,r) as c) acc -> 
-      let c' = if d == Univ.ULub then (l,Univ.UEq,r) else c in
-	Univ.UniverseConstraints.add c' acc) 
-    c Univ.UniverseConstraints.empty
+      let c' = if d == Universes.ULub then (l,Universes.UEq,r) else c in
+	Universes.Constraints.add c' acc) 
+    c Universes.Constraints.empty
 
 let constr_cmp pb sigma flags t u =
   let b, cstrs = 
-    if pb == Reduction.CONV then eq_constr_universes t u
-    else leq_constr_universes t u
+    if pb == Reduction.CONV then Universes.eq_constr_universes t u
+    else Universes.leq_constr_universes t u
   in 
     if b then 
       try Evd.add_universe_constraints sigma cstrs, b