Merge PR #6775: Allow using cumulativity without forcing strict constraints.

12 files changed, 387 insertions, 217 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index b95068ebf4..bd47a04f1e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -548,44 +548,111 @@ let fold sigma f acc c = match kind sigma c with
   | CoFix (_,(lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
 
-let compare_gen k eq_inst eq_sort eq_constr c1 c2 =
-  (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr c1 c2
+let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
+  (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2
 
 let eq_constr sigma c1 c2 =
   let kind c = kind_upto sigma c in
-  let rec eq_constr c1 c2 =
-    compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal eq_constr c1 c2
+  let rec eq_constr nargs c1 c2 =
+    compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal eq_constr nargs c1 c2
   in
-  eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
+  eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
 
 let eq_constr_nounivs sigma c1 c2 =
   let kind c = kind_upto sigma c in
-  let rec eq_constr c1 c2 =
-    compare_gen kind (fun _ _ _ -> true) (fun _ _ -> true) eq_constr c1 c2
+  let rec eq_constr nargs c1 c2 =
+    compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2
   in
-  eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
+  eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
 
 let compare_constr sigma cmp c1 c2 =
   let kind c = kind_upto sigma c in
-  let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in
-  compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr 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 test_constr_universes sigma leq m n =
+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
+  else
+    CArray.fold_left3
+      (fun cstrs v u u' ->
+         let open Univ.Variance in
+         match v with
+         | Irrelevant -> Constraints.add (UWeak (u,u')) cstrs
+         | Covariant ->
+           let u = Univ.Universe.make u in
+           let u' = Univ.Universe.make u' in
+           (match cv_pb with
+            | Reduction.CONV -> Constraints.add (UEq (u,u')) cstrs
+            | Reduction.CUMUL -> Constraints.add (ULe (u,u')) cstrs)
+         | Invariant ->
+           let u = Univ.Universe.make u in
+           let u' = Univ.Universe.make u' in
+           Constraints.add (UEq (u,u')) cstrs)
+      cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+
+let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
+  let open Universes in
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ ->
+    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
+    cstrs
+  | Declarations.Polymorphic_ind _ ->
+     enforce_eq_instances_univs false u1 u2 cstrs
+  | Declarations.Cumulative_ind cumi ->
+    let num_param_arity = Reduction.inductive_cumulativity_arguments spec in
+    let variances = Univ.ACumulativityInfo.variance cumi in
+    compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs
+
+let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
+  let open Universes in
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ ->
+    cstrs
+  | Declarations.Polymorphic_ind _ ->
+    enforce_eq_instances_univs false u1 u2 cstrs
+  | Declarations.Cumulative_ind cumi ->
+    let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in
+    if not (Int.equal num_cnstr_args nargs)
+    then enforce_eq_instances_univs false u1 u2 cstrs
+    else
+      Array.fold_left2 (fun cstrs u1 u2 -> Universes.(Constraints.add (UWeak (u1,u2)) cstrs))
+        cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2)
+
+let eq_universes env sigma cstrs cv_pb ref nargs l l' =
+  if Univ.Instance.is_empty l then (assert (Univ.Instance.is_empty l'); true)
+  else
+    let l = Evd.normalize_universe_instance sigma l
+    and l' = Evd.normalize_universe_instance sigma l' in
+    let open Universes in
+    match ref with
+    | VarRef _ -> assert false (* variables don't have instances *)
+    | ConstRef _ ->
+      cstrs := enforce_eq_instances_univs true l l' !cstrs; true
+    | IndRef ind ->
+      let mind = Environ.lookup_mind (fst ind) env in
+      cstrs := cmp_inductives cv_pb (mind,snd ind) nargs l l' !cstrs;
+      true
+    | ConstructRef ((mi,ind),ctor) ->
+      let mind = Environ.lookup_mind mi env in
+      cstrs := cmp_constructors (mind,ind,ctor) nargs l l' !cstrs;
+      true
+
+let test_constr_universes env sigma leq m n =
   let open Universes in
   let kind c = kind_upto sigma c in
   if m == n then Some Constraints.empty
-  else 
+  else
     let cstrs = ref Constraints.empty in
-    let eq_universes strict l l' = 
-      let l = EInstance.kind sigma (EInstance.make l) in
-      let l' = EInstance.kind sigma (EInstance.make l') in
-      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
-    let eq_sorts s1 s2 = 
+    let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in
+    let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l'
+    and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in
+    let eq_sorts s1 s2 =
       let s1 = ESorts.kind sigma (ESorts.make s1) in
       let s2 = ESorts.kind sigma (ESorts.make s2) in
       if Sorts.equal s1 s2 then true
       else (cstrs := Constraints.add 
-	      (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; 
+              (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
 	    true)
     in
     let leq_sorts s1 s2 = 
@@ -594,27 +661,28 @@ let test_constr_universes sigma leq m n =
       if Sorts.equal s1 s2 then true
       else 
 	(cstrs := Constraints.add 
-	   (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; 
+           (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
 	 true)
     in
-    let rec eq_constr' m n = compare_gen kind eq_universes eq_sorts eq_constr' m n in
+    let rec eq_constr' nargs m n = compare_gen kind eq_universes eq_sorts eq_constr' nargs m n in
     let res =
       if leq then
-        let rec compare_leq m n =
-          Constr.compare_head_gen_leq_with kind kind eq_universes leq_sorts eq_constr' leq_constr' m n
-        and leq_constr' m n = m == n || compare_leq m n in
-        compare_leq m n
+        let rec compare_leq nargs m n =
+          Constr.compare_head_gen_leq_with kind kind leq_universes leq_sorts
+            eq_constr' leq_constr' nargs m n
+        and leq_constr' nargs m n = m == n || compare_leq nargs m n in
+        compare_leq 0 m n
       else
-        Constr.compare_head_gen_with kind kind eq_universes eq_sorts eq_constr' m n
+        Constr.compare_head_gen_with kind kind eq_universes eq_sorts eq_constr' 0 m n
     in
     if res then Some !cstrs else None
 
-let eq_constr_universes sigma m n =
-  test_constr_universes sigma false (unsafe_to_constr m) (unsafe_to_constr n)
-let leq_constr_universes sigma m n =
-  test_constr_universes sigma true (unsafe_to_constr m) (unsafe_to_constr n)
+let eq_constr_universes env sigma m n =
+  test_constr_universes env sigma false (unsafe_to_constr m) (unsafe_to_constr n)
+let leq_constr_universes env sigma m n =
+  test_constr_universes env sigma true (unsafe_to_constr m) (unsafe_to_constr n)
 
-let compare_head_gen_proj env sigma equ eqs eqc' m n =
+let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
   let kind c = kind_upto sigma c in
   match kind_upto sigma m, kind_upto sigma n with
   | Proj (p, c), App (f, args)
@@ -624,29 +692,28 @@ let compare_head_gen_proj env sigma equ eqs eqc' m n =
           let pb = Environ.lookup_projection p env in
           let npars = pb.Declarations.proj_npars in
 	  if Array.length args == npars + 1 then
-	    eqc' c args.(npars)
+            eqc' 0 c args.(npars)
 	  else false
       | _ -> false)
-  | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' m n
+  | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n
 
 let eq_constr_universes_proj env sigma m n =
   let open Universes in
   if m == n then Some Constraints.empty
   else 
     let cstrs = ref Constraints.empty in
-    let eq_universes strict l l' = 
-      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
-    let eq_sorts s1 s2 = 
+    let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in
+    let eq_sorts s1 s2 =
       if Sorts.equal s1 s2 then true
       else
 	(cstrs := Constraints.add 
-	   (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
+           (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs;
 	 true)
     in
-    let rec eq_constr' m n = 
-      m == n ||	compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' m n
+    let rec eq_constr' nargs m n =
+      m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n
     in
-    let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
+    let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in
     if res then Some !cstrs else None
 
 let universes_of_constr env sigma c =
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 36b6093d0f..28c9dd3c21 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -198,9 +198,12 @@ val whd_evar : Evd.evar_map -> constr -> constr
 
 val eq_constr : Evd.evar_map -> t -> t -> bool
 val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
-val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option
-val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+
+(** [eq_constr_universes_proj] can equate projections and their eta-expanded constant form. *)
 val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+
 val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
 
 (** {6 Iterators} *)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6b3ce048f7..9cf81eccea 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -813,6 +813,33 @@ let subterm_source evk (loc,k) =
     | _ -> evk in
   (loc,Evar_kinds.SubEvar evk)
 
+(* 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 = 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, 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)
+      (cstrs,soft) variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+  in
+  match Evd.add_constraints sigma cstrs with
+  | sigma ->
+    Inl (Evd.add_universe_constraints sigma soft)
+  | exception Univ.UniverseInconsistency p -> Inr p
+
+let compare_constructor_instances evd u 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/evarutil.mli b/engine/evarutil.mli
index 373875bd05..e289ca1692 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -203,6 +203,20 @@ val kind_of_term_upto : evar_map -> Constr.constr ->
     assumed to be an extention of those in [sigma1]. *)
 val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool
 
+(** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
+   [Inl sigma'] where [sigma'] is [sigma] augmented with universe
+   constraints such that [u1 cv_pb? u2] according to [variance].
+   Additionally flexible universes in irrelevant positions are unified
+   if possible. Returns [Inr p] when the former is impossible. *)
+val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array ->
+  Univ.Instance.t -> Univ.Instance.t -> evar_map ->
+  (evar_map, Univ.univ_inconsistency) Util.union
+
+(** We should only compare constructors at convertible types, so this
+   is only an opportunity to unify universes. *)
+val compare_constructor_instances : evar_map ->
+  Univ.Instance.t -> Univ.Instance.t -> evar_map
+
 (** {6 Removing hyps in evars'context}
 raise OccurHypInSimpleClause if the removal breaks dependencies *)
 
diff --git a/engine/evd.ml b/engine/evd.ml
index b7b87370e2..f6e13e1f43 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -857,15 +857,10 @@ let set_eq_sort env d s1 s2 =
   | Some (u1, u2) ->
     if not (type_in_type env) then
       add_universe_constraints d
-        (Universes.Constraints.singleton (u1,Universes.UEq,u2))
+        (Universes.Constraints.singleton (Universes.UEq (u1,u2)))
     else
       d
 
-let has_lub evd u1 u2 =
-  if Univ.Universe.equal u1 u2 then evd
-  else add_universe_constraints evd
-    (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)
 
@@ -883,7 +878,7 @@ let set_leq_sort env evd s1 s2 =
   | None -> evd
   | Some (u1, u2) ->
      if not (type_in_type env) then
-       add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
+       add_universe_constraints evd (Universes.Constraints.singleton (Universes.ULe (u1,u2)))
      else evd
 	    
 let check_eq evd s s' =
diff --git a/engine/evd.mli b/engine/evd.mli
index bd9d75c6b0..911799c447 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -583,7 +583,6 @@ val normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t
 
 val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
 val set_eq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
-val has_lub : evar_map -> Univ.Universe.t -> Univ.Universe.t -> evar_map
 val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
 val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
 val set_eq_instances : ?flex:bool -> 
diff --git a/engine/termops.ml b/engine/termops.ml
index 35258762a7..3dfb0c34fd 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
@@ -914,12 +916,9 @@ let vars_of_global_reference env gr =
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
-let dependent_main noevar univs sigma m t =
+let dependent_main noevar sigma m t =
   let open EConstr in
-  let eqc x y =
-    if univs then not (Option.is_empty (eq_constr_universes sigma x y))
-    else eq_constr_nounivs sigma x y
-  in
+  let eqc x y = eq_constr_nounivs sigma x y in
   let rec deprec m t =
     if eqc m t then
       raise Occur
@@ -936,11 +935,8 @@ let dependent_main noevar univs sigma m t =
   in
   try deprec m t; false with Occur -> true
 
-let dependent sigma c t = dependent_main false false sigma c t
-let dependent_no_evar sigma c t = dependent_main true false sigma c t
-
-let dependent_univs sigma c t = dependent_main false true sigma c t
-let dependent_univs_no_evar sigma c t = dependent_main true true sigma c t
+let dependent sigma c t = dependent_main false sigma c t
+let dependent_no_evar sigma c t = dependent_main true sigma c t
 
 let dependent_in_decl sigma a decl =
   let open NamedDecl in
diff --git a/engine/termops.mli b/engine/termops.mli
index ef3cb91be6..3b0c4bba64 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -108,8 +108,6 @@ val free_rels : Evd.evar_map -> constr -> Int.Set.t
 (** [dependent m t] tests whether [m] is a subterm of [t] *)
 val dependent : Evd.evar_map -> constr -> constr -> bool
 val dependent_no_evar : Evd.evar_map -> constr -> constr -> bool
-val dependent_univs : Evd.evar_map -> constr -> constr -> bool
-val dependent_univs_no_evar : Evd.evar_map -> constr -> constr -> bool
 val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool
 val count_occurrences : Evd.evar_map -> constr -> constr -> int
 val collect_metas : Evd.evar_map -> constr -> int list
diff --git a/engine/uState.ml b/engine/uState.ml
index e57afd743a..1dd8acd0db 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,11 +148,21 @@ 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 normalize = Universes.normalize_universe_opt_subst vars 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
   let is_local l = Univ.LMap.mem l !vars in
   let varinfo x =
     match Univ.Universe.level x with
@@ -185,12 +201,12 @@ let process_universe_constraints ctx cstrs =
     if UGraph.check_eq univs l r then local
     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
   in
-  let unify_universes (l, d, r) local =
-    let l = normalize l and r = normalize r in
-      if Univ.Universe.equal l r then local
+  let unify_universes cst local =
+    let cst = nf_constraint cst in
+      if Constraints.is_trivial cst then local
       else 
-          match d with
-          | Universes.ULe ->
+          match cst with
+          | ULe (l, r) ->
             if UGraph.check_leq univs l r then
               (** Keep Prop/Set <= var around if var might be instantiated by prop or set
                   later. *)
@@ -218,43 +234,47 @@ let process_universe_constraints ctx cstrs =
                 else
                   Univ.enforce_leq l r local
               end
-          | Universes.ULub ->
-            begin match Universe.level l, Universe.level r with
-            | Some l', Some r' ->
-              equalize_variables true l l' r r' local
-            | _, _ -> assert false
-            end
-          | Universes.UEq -> equalize_universes l r local
+          | 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 = 
-    Universes.Constraints.fold unify_universes cstrs Univ.Constraint.empty
+    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
   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, Universes.ULe, r)
-      else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r)
+    let cstr' = match d with
+      | Univ.Lt ->
+        Universes.ULe (Univ.Universe.super l, r)
+      | Univ.Le -> Universes.ULe (l, r)
+      | Univ.Eq -> Universes.UEq (l, r)
     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
@@ -563,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
@@ -582,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';
@@ -601,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)
@@ -614,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 9a2bc706be..48c38fafc8 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 c744674053..ddc9beff49 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)  ->
@@ -114,53 +117,60 @@ let universe_binders_with_opt_names ref levels = function
 let set_minimization = ref true
 let is_set_minimization () = !set_minimization
 			    
-type universe_constraint_type = ULe | UEq | ULub
-
-type universe_constraint = Universe.t * universe_constraint_type * Universe.t
+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(
   struct 
     type t = universe_constraint
 
-    let compare_type c c' =
-      match c, c' with
-      | ULe, ULe -> 0
-      | ULe, _ -> -1
-      | _, ULe -> 1
-      | UEq, UEq -> 0
-      | UEq, _ -> -1
-      | ULub, ULub -> 0
-      | ULub, _ -> 1
-      
-    let compare (u,c,v) (u',c',v') =
-      let i = compare_type c c' in
-	if Int.equal i 0 then
-	  let i' = Universe.compare u u' in
-	    if Int.equal i' 0 then Universe.compare v v'
-	    else 
-	      if c != ULe && Universe.compare u v' = 0 && Universe.compare v u' = 0 then 0
-	      else i'
-	else i
+    let compare x y =
+      match x, y with
+      | ULe (u, v), ULe (u', v') ->
+        let i = Universe.compare u u' in
+        if Int.equal i 0 then Universe.compare v v'
+        else i
+      | UEq (u, v), UEq (u', v') ->
+        let i = Universe.compare u u' in
+        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') | 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
+        else i
+      | ULe _, _ -> -1
+      | _, ULe _ -> 1
+      | UEq _, _ -> -1
+      | _, UEq _ -> 1
+      | ULub _, _ -> -1
+      | _, ULub _ -> 1
   end)
   
   include S
-  
-  let add (l,d,r as cst) s = 
-    if Universe.equal l r then s
-    else add cst s
 
-  let tr_dir = function
-    | ULe -> Le
-    | UEq -> Eq
-    | ULub -> Eq
+  let is_trivial = function
+    | ULe (u, v) | UEq (u, v) -> Universe.equal u v
+    | ULub (u, v) | UWeak (u, v) -> Level.equal u v
 
-  let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ "
+  let add cst s =
+    if is_trivial cst then s
+    else add cst s
+
+  let pr_one = function
+    | 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 (u1,op,u2) pp_std ->
-	pp_std ++ Universe.pr u1 ++ str (op_str op) ++
-	Universe.pr u2 ++ fnl ()) c (str "")
+    fold (fun cst pp_std ->
+        pp_std ++ pr_one cst ++ fnl ()) c (str "")
 
   let equal x y = 
     x == y || equal x y
@@ -174,13 +184,13 @@ type 'a universe_constrained = 'a * universe_constraints
 type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
 
 let enforce_eq_instances_univs strict x y c = 
-  let d = if strict then ULub else UEq in
+  let mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in
   let ax = Instance.to_array x and ay = Instance.to_array y in
     if Array.length ax != Array.length ay then
       CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
 	       Pp.str " instances of different lengths.");
     CArray.fold_right2
-      (fun x y -> Constraints.add (Universe.make x, d, Universe.make y))
+      (fun x y -> Constraints.add (mk x y))
       ax ay c
 
 let enforce_univ_constraint (u,d,v) =
@@ -207,30 +217,65 @@ let subst_univs_constraints subst csts =
     (fun c cstrs -> subst_univs_constraint subst c cstrs)
     csts Constraint.empty
 
-let subst_univs_universe_constraint fn (u,d,v) =
-  let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
+let level_subst_of f =
+  fun l ->
+    try let u = f l in
+          match Universe.level u with
+          | None -> l
+          | Some l -> l
+    with Not_found -> l
+
+let subst_univs_universe_constraint fn = function
+  | ULe (u, v) ->
+    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
+    if Universe.equal u' v' then None
+    else Some (ULe (u',v'))
+  | UEq (u, v) ->
+    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
     if Universe.equal u' v' then None
-    else Some (u',d,v')
+    else Some (ULe (u',v'))
+  | ULub (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 (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 tr (x,d,y) acc =
-    let add l d l' acc = Constraint.add (l,Constraints.tr_dir d,l') acc in
-      match Universe.level x, d, Universe.level y with
-      | Some l, (ULe | UEq | ULub), Some l' -> add l d l' acc
-      | _, ULe, Some l' -> enforce_leq x y acc
-      | _, ULub, _ -> acc
-      | _, d, _ -> 
-	let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in
-	  if f g x y then acc else 
-	    raise (Invalid_argument 
-		   "to_constraints: non-trivial algebraic constraint between universes")
-  in Constraints.fold tr s Constraint.empty
+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
+        | None, Some _ -> enforce_leq l l' acc
+        | _, None ->
+          if UGraph.check_leq g l l'
+          then acc
+          else invalid ()
+      end
+    | UEq (l, l') ->
+      begin match Universe.level l, Universe.level l' with
+        | Some l, Some l' -> Constraint.add (l, Eq, l') acc
+        | None, _ | _, None ->
+          if UGraph.check_eq g l l'
+          then acc
+          else invalid ()
+      end
+  in
+  Constraints.fold tr s Constraint.empty
 
 (** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
     to expose subterms of [m] and [n], arguments. *)
@@ -242,54 +287,21 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
      [kind1,kind2], because [kind1] and [kind2] may be different,
      typically evaluating [m] and [n] in different evar maps. *)
   let cstrs = ref accu in
-  let eq_universes strict = UGraph.check_eq_instances univs in
+  let eq_universes _ _ = UGraph.check_eq_instances univs in
   let eq_sorts s1 s2 = 
     if Sorts.equal s1 s2 then true
     else
       let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-      match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
+      match fold (Constraints.singleton (UEq (u1, u2))) !cstrs with
       | None -> false
       | Some accu -> cstrs := accu; true
   in
-  let rec eq_constr' m n = 
-    Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n
+  let rec eq_constr' nargs m n =
+    Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' nargs m n
   in
-  let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
+  let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in
   if res then Some !cstrs else None
 
-let compare_head_gen_proj env equ eqs eqc' m n =
-  match kind m, kind n with
-  | Proj (p, c), App (f, args)
-  | App (f, args), Proj (p, c) -> 
-      (match kind f with
-      | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
-          let pb = Environ.lookup_projection p env in
-          let npars = pb.Declarations.proj_npars in
-	  if Array.length args == npars + 1 then
-	    eqc' c args.(npars)
-	  else false
-      | _ -> false)
-  | _ -> Constr.compare_head_gen equ eqs eqc' m n
-      
-let eq_constr_universes_proj env m n =
-  if m == n then true, Constraints.empty
-  else 
-    let cstrs = ref Constraints.empty in
-    let eq_universes strict l l' = 
-      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
-    let eq_sorts s1 s2 = 
-      if Sorts.equal s1 s2 then true
-      else
-	(cstrs := Constraints.add 
-	   (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
-	 true)
-    in
-    let rec eq_constr' m n = 
-      m == n ||	compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n
-    in
-    let res = eq_constr' m n in
-    res, !cstrs
-
 (* Generator of levels *)
 type universe_id = DirPath.t * int
 
@@ -545,14 +557,6 @@ let choose_canonical ctx flexible algs s =
 	      let canon = LSet.choose algs in
 		canon, (global, rigid, LSet.remove canon flexible)
 
-let level_subst_of f =
-  fun l ->
-    try let u = f l in
-          match Universe.level u with
-          | None -> l
-          | Some l -> l
-    with Not_found -> l
-
 let subst_univs_fn_constr f c =
   let changed = ref false in
   let fu = Univ.subst_univs_universe f in
@@ -914,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 *)
@@ -934,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)
@@ -972,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 -> 
@@ -984,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 8e6b8f60c9..4823c57463 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,14 +72,21 @@ 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_type = ULe | UEq | ULub
+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
 
-type universe_constraint = Universe.t * universe_constraint_type * Universe.t
 module Constraints : sig
   include Set.S with type elt = universe_constraint
 
+  val is_trivial : universe_constraint -> bool
+
   val pr : t -> Pp.t
 end
 
@@ -92,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
@@ -102,10 +114,6 @@ val eq_constr_univs_infer_with :
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
   UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
 
-(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
-    application grouping and the universe constraints in [c]. *)
-val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained
-
 (** Build a fresh instance for a given context, its associated substitution and 
     the instantiated constraints. *)
 
@@ -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 ->