Delayed weak constraints for cumulative inductive types.

When comparing 2 irrelevant universes [u] and [v] we add a "weak
constraint" [UWeak(u,v)] to the UState. Then at minimization time a
weak constraint between unrelated universes where one is flexible
causes them to be unified.

8 files changed, 126 insertions, 52 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 0d55b92c2..3ee072214 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -570,8 +570,6 @@ let compare_constr sigma cmp c1 c2 =
   let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in
   compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
 
-let cumul_weak_constraints = ref true
-
 let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
   let open Universes in
   if not nargs_ok then enforce_eq_instances_univs false u u' cstrs
@@ -580,7 +578,7 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
       (fun cstrs v u u' ->
          let open Univ.Variance in
          match v with
-         | Irrelevant -> if !cumul_weak_constraints then Constraints.add (ULub (u,u')) cstrs else cstrs
+         | Irrelevant -> Constraints.add (UWeak (u,u')) cstrs
          | Covariant ->
            let u = Univ.Universe.make u in
            let u' = Univ.Universe.make u' in
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 87531e116..28c9dd3c2 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -196,8 +196,6 @@ val whd_evar : Evd.evar_map -> constr -> constr
 
 (** {6 Equality} *)
 
-val cumul_weak_constraints : bool ref
-
 val eq_constr : Evd.evar_map -> t -> t -> bool
 val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
 val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index fdb14b725..9cf81ecce 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -813,20 +813,16 @@ let subterm_source evk (loc,k) =
     | _ -> evk in
   (loc,Evar_kinds.SubEvar evk)
 
-let try_soft evd u u' =
-  let open Universes in
-  try Evd.add_universe_constraints evd (Constraints.singleton (ULub (u, u')))
-  with UState.UniversesDiffer | Univ.UniverseInconsistency _ -> evd
-
 (* Add equality constraints for covariant/invariant positions. For
    irrelevant positions, unify universes when flexible. *)
 let compare_cumulative_instances cv_pb variances u u' sigma =
+  let open Universes in
   let cstrs = Univ.Constraint.empty in
-  let soft = [] in
+  let soft = Constraints.empty in
   let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' ->
       let open Univ.Variance in
       match v with
-      | Irrelevant -> cstrs, if !EConstr.cumul_weak_constraints then (u,u')::soft else soft
+      | Irrelevant -> cstrs, Constraints.add (UWeak (u,u')) soft
       | Covariant when cv_pb == Reduction.CUMUL ->
         Univ.Constraint.add (u,Univ.Le,u') cstrs, soft
       | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft)
@@ -834,12 +830,16 @@ let compare_cumulative_instances cv_pb variances u u' sigma =
   in
   match Evd.add_constraints sigma cstrs with
   | sigma ->
-    Inl (List.fold_left (fun sigma (u,u') -> try_soft sigma u u') sigma soft)
+    Inl (Evd.add_universe_constraints sigma soft)
   | exception Univ.UniverseInconsistency p -> Inr p
 
 let compare_constructor_instances evd u u' =
-  Array.fold_left2 try_soft
-    evd (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+  let open Universes in
+  let soft =
+    Array.fold_left2 (fun cs u u' -> Constraints.add (UWeak (u,u')) cs)
+      Constraints.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+  in
+  Evd.add_universe_constraints evd soft
 
 (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
     [u] up to existential variable instantiation and equalisable
diff --git a/engine/termops.ml b/engine/termops.ml
index 20b6b3504..3dfb0c34f 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -302,7 +302,9 @@ let pr_evar_universe_context ctx =
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
      h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
-       h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
+     h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++
+     str "WEAK CONSTRAINTS:"++brk(0,1)++
+     h 0 (UState.pr_weak prl ctx) ++ fnl ())
 
 let print_env_short env =
   let print_constr = print_kconstr in
diff --git a/engine/uState.ml b/engine/uState.ml
index 8111ebffe..1dd8acd0d 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -20,6 +20,8 @@ type uinfo = {
   uloc : Loc.t option;
 }
 
+module UPairSet = Universes.UPairSet
+
 (* 2nd part used to check consistency on the fly. *)
 type t =
  { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t;
@@ -32,6 +34,7 @@ type t =
         algebraic universes as they appear in inferred types only. *)
    uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
    uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
+   uctx_weak_constraints : UPairSet.t
  }
   
 let empty =
@@ -41,7 +44,8 @@ let empty =
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
     uctx_universes = UGraph.initial_universes;
-    uctx_initial_universes = UGraph.initial_universes; }
+    uctx_initial_universes = UGraph.initial_universes;
+    uctx_weak_constraints = UPairSet.empty; }
 
 let make u =
     { empty with 
@@ -69,6 +73,7 @@ let union ctx ctx' =
     let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
                                (Univ.ContextSet.levels ctx.uctx_local) in
     let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
+    let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in
     let declarenew g =
       Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
     in
@@ -82,10 +87,11 @@ let union ctx ctx' =
           Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
         uctx_initial_universes = declarenew ctx.uctx_initial_universes;
         uctx_universes = 
-          if local == ctx.uctx_local then ctx.uctx_universes
-          else
-            let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-            UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
+          (if local == ctx.uctx_local then ctx.uctx_universes
+           else
+             let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
+             UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes));
+        uctx_weak_constraints = weak}
 
 let context_set ctx = ctx.uctx_local
 
@@ -142,14 +148,18 @@ let instantiate_variable l b v =
 
 exception UniversesDiffer
 
+let drop_weak_constraints = ref false
+
 let process_universe_constraints ctx cstrs =
   let open Univ in
   let open Universes in
   let univs = ctx.uctx_universes in
   let vars = ref ctx.uctx_univ_variables in
+  let weak = ref ctx.uctx_weak_constraints in
   let normalize = normalize_univ_variable_opt_subst vars in
   let nf_constraint = function
     | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
+    | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v)
     | UEq (u, v) -> UEq (subst_univs_universe normalize u, subst_univs_universe normalize v)
     | ULe (u, v) -> ULe (subst_univs_universe normalize u, subst_univs_universe normalize v)
   in
@@ -226,12 +236,14 @@ let process_universe_constraints ctx cstrs =
               end
           | ULub (l, r) ->
               equalize_variables true (Universe.make l) l (Universe.make r) r local
+          | UWeak (l, r) ->
+            if not !drop_weak_constraints then weak := UPairSet.add (l,r) !weak; local
           | UEq (l, r) -> equalize_universes l r local
   in
   let local = 
     Constraints.fold unify_universes cstrs Univ.Constraint.empty
   in
-    !vars, local
+    !vars, !weak, local
 
 let add_constraints ctx cstrs =
   let univs, local = ctx.uctx_local in
@@ -245,20 +257,24 @@ let add_constraints ctx cstrs =
     in Universes.Constraints.add cstr' acc)
     cstrs Universes.Constraints.empty
   in
-  let vars, local' = process_universe_constraints ctx cstrs' in
-    { ctx with uctx_local = (univs, Univ.Constraint.union local local');
-      uctx_univ_variables = vars;
-      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
+  let vars, weak, local' = process_universe_constraints ctx cstrs' in
+  { ctx with
+    uctx_local = (univs, Univ.Constraint.union local local');
+    uctx_univ_variables = vars;
+    uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes;
+    uctx_weak_constraints = weak; }
 
 (* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *)
 (* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *)
 
 let add_universe_constraints ctx cstrs =
   let univs, local = ctx.uctx_local in
-  let vars, local' = process_universe_constraints ctx cstrs in
-    { ctx with uctx_local = (univs, Univ.Constraint.union local local');
-      uctx_univ_variables = vars;
-      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
+  let vars, weak, local' = process_universe_constraints ctx cstrs in
+  { ctx with
+    uctx_local = (univs, Univ.Constraint.union local local');
+    uctx_univ_variables = vars;
+    uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes;
+    uctx_weak_constraints = weak; }
 
 let constrain_variables diff ctx =
   let univs, local = ctx.uctx_local in
@@ -567,16 +583,18 @@ let fix_undefined_variables uctx =
 
 let refresh_undefined_univ_variables uctx =
   let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
-  let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) 
+  let subst_fn u = Univ.subst_univs_level_level subst u in
+  let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc)
     uctx.uctx_univ_algebraic Univ.LSet.empty 
   in
   let vars = 
     Univ.LMap.fold
       (fun u v acc ->
-        Univ.LMap.add (Univ.subst_univs_level_level subst u) 
+        Univ.LMap.add (subst_fn u)
           (Option.map (Univ.subst_univs_level_universe subst) v) acc)
       uctx.uctx_univ_variables Univ.LMap.empty
   in
+  let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in
   let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g)
                                    (Univ.ContextSet.levels ctx') g in
   let initial = declare uctx.uctx_initial_universes in
@@ -586,18 +604,20 @@ let refresh_undefined_univ_variables uctx =
                uctx_seff_univs = uctx.uctx_seff_univs;
                uctx_univ_variables = vars; uctx_univ_algebraic = alg;
                uctx_universes = univs;
-               uctx_initial_universes = initial } in
+               uctx_initial_universes = initial;
+               uctx_weak_constraints = weak; } in
     uctx', subst
 
 let minimize uctx =
-  let ((vars',algs'), us') = 
-    Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
-				    uctx.uctx_univ_algebraic
+  let open Universes in
+  let ((vars',algs'), us') =
+    normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
+      uctx.uctx_univ_algebraic uctx.uctx_weak_constraints
   in
   if Univ.ContextSet.equal us' uctx.uctx_local then uctx
   else
     let us', universes =
-      Universes.refresh_constraints uctx.uctx_initial_universes us'
+      refresh_constraints uctx.uctx_initial_universes us'
     in
       { uctx_names = uctx.uctx_names;
         uctx_local = us';
@@ -605,7 +625,8 @@ let minimize uctx =
         uctx_univ_variables = vars'; 
         uctx_univ_algebraic = algs';
         uctx_universes = universes;
-        uctx_initial_universes = uctx.uctx_initial_universes }
+        uctx_initial_universes = uctx.uctx_initial_universes;
+        uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) }
 
 let universe_of_name uctx s = 
   UNameMap.find s (fst uctx.uctx_names)
@@ -618,5 +639,9 @@ let update_sigma_env uctx env =
   in
   merge true univ_rigid eunivs eunivs.uctx_local
 
+let pr_weak prl {uctx_weak_constraints=weak} =
+  let open Pp in
+  prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak)
+
 (** Deprecated *)
 let normalize = minimize
diff --git a/engine/uState.mli b/engine/uState.mli
index 9a2bc706b..48c38fafc 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -72,6 +72,8 @@ val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
 
 (** {5 Constraints handling} *)
 
+val drop_weak_constraints : bool ref
+
 val add_constraints : t -> Univ.Constraint.t -> t
 (**
   @raise UniversesDiffer when universes differ
@@ -164,3 +166,5 @@ val update_sigma_env : t -> Environ.env -> t
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
 val reference_of_level : t -> Univ.Level.t -> Libnames.reference
+
+val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/universes.ml b/engine/universes.ml
index ae5eef067..ddc9beff4 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -18,6 +18,9 @@ open Univ
 open Globnames
 open Nametab
 
+module UPairs = OrderedType.UnorderedPair(Univ.Level)
+module UPairSet = Set.Make (UPairs)
+
 let reference_of_level l =
   match Level.name l with
   | Some (d, n as na)  ->
@@ -118,6 +121,7 @@ type universe_constraint =
   | ULe of Universe.t * Universe.t
   | UEq of Universe.t * Universe.t
   | ULub of Level.t * Level.t
+  | UWeak of Level.t * Level.t
 
 module Constraints = struct
   module S = Set.Make(
@@ -135,7 +139,7 @@ module Constraints = struct
         if Int.equal i 0 then Universe.compare v v'
         else if Universe.equal u v' && Universe.equal v u' then 0
         else i
-      | ULub (u, v), ULub (u', v') ->
+      | ULub (u, v), ULub (u', v') | UWeak (u, v), UWeak (u', v') ->
         let i = Level.compare u u' in
         if Int.equal i 0 then Level.compare v v'
         else if Level.equal u v' && Level.equal v u' then 0
@@ -144,13 +148,15 @@ module Constraints = struct
       | _, ULe _ -> 1
       | UEq _, _ -> -1
       | _, UEq _ -> 1
+      | ULub _, _ -> -1
+      | _, ULub _ -> 1
   end)
   
   include S
 
   let is_trivial = function
     | ULe (u, v) | UEq (u, v) -> Universe.equal u v
-    | ULub (u, v) -> Level.equal u v
+    | ULub (u, v) | UWeak (u, v) -> Level.equal u v
 
   let add cst s =
     if is_trivial cst then s
@@ -160,6 +166,7 @@ module Constraints = struct
     | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v
     | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v
     | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v
+    | UWeak (u, v) -> Level.pr u ++ str " ~ " ++ Level.pr v
 
   let pr c =
     fold (fun cst pp_std ->
@@ -231,19 +238,25 @@ let subst_univs_universe_constraint fn = function
     let u' = level_subst_of fn u and v' = level_subst_of fn v in
     if Level.equal u' v' then None
     else Some (ULub (u',v'))
+  | UWeak (u, v) ->
+    let u' = level_subst_of fn u and v' = level_subst_of fn v in
+    if Level.equal u' v' then None
+    else Some (UWeak (u',v'))
 
 let subst_univs_universe_constraints subst csts =
   Constraints.fold 
     (fun c -> Option.fold_right Constraints.add (subst_univs_universe_constraint subst c))
     csts Constraints.empty 
 
-let to_constraints g s =
+let to_constraints ~force_weak g s =
   let invalid () =
     raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes")
   in
   let tr cst acc =
     match cst with
     | ULub (l, l') -> Constraint.add (l, Eq, l') acc
+    | UWeak (l, l') when force_weak -> Constraint.add (l, Eq, l') acc
+    | UWeak  _-> acc
     | ULe (l, l') ->
       begin match Universe.level l, Universe.level l' with
         | Some l, Some l' -> Constraint.add (l, Le, l') acc
@@ -905,7 +918,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
       else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs)
       us (ctx, us, algs, lbounds, cstrs)
 
-let normalize_context_set ctx us algs = 
+let normalize_context_set g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   let uf = UF.create () in
   (** Keep the Prop/Set <= i constraints separate for minimization *)
@@ -925,7 +938,7 @@ let normalize_context_set ctx us algs =
 	else (smallles, Constraint.add cstr noneqs))
     csts (Constraint.empty, Constraint.empty)
   in
-  let csts = 
+  let csts =
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
     let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g)
@@ -963,7 +976,7 @@ let normalize_context_set ctx us algs =
   let noneqs = Constraint.union noneqs smallles in
   let partition = UF.partition uf in
   let flex x = LMap.mem x us in
-  let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s -> 
+  let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s ->
     let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
     (* Add equalities for globals which can't be merged anymore. *)
     let cstrs = LSet.fold (fun g cst -> 
@@ -975,16 +988,41 @@ let normalize_context_set ctx us algs =
       Constraint.add (canon, Univ.Eq, g) cst) rigid
       cstrs
     in
-    let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in
-    let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in
     let canonu = Some (Universe.make canon) in
     let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in
-      (LSet.diff ctx flexible, subst, us, cstrs))
-    (ctx, LMap.empty, us, Constraint.empty) partition
+      (LSet.diff ctx flexible, us, cstrs))
+    (ctx, us, Constraint.empty) partition
   in
+  (* Process weak constraints: when one side is flexible and the 2
+     universes are unrelated unify them. *)
+  let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) ->
+      let norm = let us = ref us in level_subst_of (normalize_univ_variable_opt_subst us) in
+      let u = norm u and v = norm v in
+      let set_to a b =
+        (LSet.remove a ctx,
+         LMap.add a (Some (Universe.make b)) us,
+         UGraph.enforce_constraint (a,Eq,b) g)
+      in
+      if UGraph.check_constraint g (u,Le,v) || UGraph.check_constraint g (v,Le,u)
+      then acc
+      else
+      if LMap.mem u us
+      then set_to u v
+      else if LMap.mem v us
+      then set_to v u
+      else acc)
+      weak (ctx, us, g)  in
   (* Noneqs is now in canonical form w.r.t. equality constraints, 
      and contains only inequality constraints. *)
-  let noneqs = subst_univs_level_constraints subst noneqs in
+  let noneqs =
+    let us = ref us in
+    let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
+    Constraint.fold (fun (u,d,v) noneqs ->
+        let u = norm u and v = norm v in
+        if d != Lt && Level.equal u v then noneqs
+        else Constraint.add (u,d,v) noneqs)
+      noneqs Constraint.empty
+  in
   (* Compute the left and right set of flexible variables, constraints
      mentionning other variables remain in noneqs. *)
   let noneqs, ucstrsl, ucstrsr = 
diff --git a/engine/universes.mli b/engine/universes.mli
index 4af944347..4823c5746 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -14,6 +14,9 @@ open Constr
 open Environ
 open Univ
 
+(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *)
+module UPairSet : CSet.S with type elt = (Level.t * Level.t)
+
 val set_minimization : bool ref
 val is_set_minimization : unit -> bool
 
@@ -69,12 +72,15 @@ val new_sort_in_family : Sorts.family -> Sorts.t
     When doing conversion of universes, not only do we have =/<= constraints but
     also Lub constraints which correspond to unification of two levels which might
     not be necessary if unfolding is performed.
+
+    UWeak constraints come from irrelevant universes in cumulative polymorphism.
 *)
 
 type universe_constraint =
   | ULe of Universe.t * Universe.t
   | UEq of Universe.t * Universe.t
   | ULub of Level.t * Level.t
+  | UWeak of Level.t * Level.t
 
 module Constraints : sig
   include Set.S with type elt = universe_constraint
@@ -96,7 +102,9 @@ val subst_univs_universe_constraints : universe_subst_fn ->
 
 val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function
 
-val to_constraints : UGraph.t -> Constraints.t -> Constraint.t
+(** With [force_weak] UWeak constraints are turned into equalities,
+   otherwise they're forgotten. *)
+val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t
 
 (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
     {!eq_constr_univs_infer} taking kind-of-term functions, to expose
@@ -167,9 +175,10 @@ val make_opt_subst : universe_opt_subst -> universe_subst_fn
 
 val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
 
-val normalize_context_set : ContextSet.t -> 
+val normalize_context_set : UGraph.t -> ContextSet.t ->
   universe_opt_subst (* The defined and undefined variables *) ->
-  LSet.t (* univ variables that can be substituted by algebraics *) -> 
+  LSet.t (* univ variables that can be substituted by algebraics *) ->
+  UPairSet.t (* weak equality constraints *) ->
   (universe_opt_subst * LSet.t) in_universe_context_set
 
 val normalize_univ_variables : universe_opt_subst ->