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

40 files changed, 1020 insertions, 482 deletions

diff --git a/CHANGES b/CHANGES
index 25a519f15..63913bff5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -95,6 +95,10 @@ Universes
 - Universe cumulativity for inductive types is now specified as a
   variance for each polymorphic universe. See the reference manual for
   more information.
+- Inference of universe constraints with cumulative inductive types
+  produces more general constraints. Unsetting new option Cumulativity
+  Weak Constraints produces even more general constraints (but may
+  produce too many universes to be practical).
 - Fix #5726: Notations that start with `Type` now support universe instances
   with `@{u}`.
 - `with Definition` now understands universe declarations
diff --git a/clib/clib.mllib b/clib/clib.mllib
index 0b5d9826f..c9b4d72fc 100644
--- a/clib/clib.mllib
+++ b/clib/clib.mllib
@@ -5,6 +5,7 @@ CEphemeron
 Hashset
 Hashcons
 
+OrderedType
 CSet
 CMap
 CList
diff --git a/clib/orderedType.ml b/clib/orderedType.ml
new file mode 100644
index 000000000..922eb76ab
--- /dev/null
+++ b/clib/orderedType.ml
@@ -0,0 +1,35 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+module type S =
+sig
+  type t
+  val compare : t -> t -> int
+end
+
+module Pair (M:S) (N:S) = struct
+  type t = M.t * N.t
+
+  let compare (a,b) (a',b') =
+    let i = M.compare a a' in
+    if Int.equal i 0 then N.compare b b'
+    else i
+end
+
+module UnorderedPair (M:S) = struct
+  type t = M.t * M.t
+
+  let reorder (a,b as p) =
+    if M.compare a b <= 0 then p else (b,a)
+
+  let compare p p' =
+    let p = reorder p and p' = reorder p' in
+    let module P = Pair(M)(M) in P.compare p p'
+end
diff --git a/clib/orderedType.mli b/clib/orderedType.mli
new file mode 100644
index 000000000..3578ea0d8
--- /dev/null
+++ b/clib/orderedType.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+module type S =
+sig
+  type t
+  val compare : t -> t -> int
+end
+
+module Pair (M:S) (N:S) : S with type t = M.t * N.t
+
+module UnorderedPair (M:S) : S with type t = M.t * M.t
diff --git a/dev/ci/user-overlays/06775-univ-cumul-weak.sh b/dev/ci/user-overlays/06775-univ-cumul-weak.sh
new file mode 100644
index 000000000..8afcbf78a
--- /dev/null
+++ b/dev/ci/user-overlays/06775-univ-cumul-weak.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "6775" ] || [ "$CI_BRANCH" = "univ-cumul" ]; then
+    Elpi_CI_BRANCH=coq-master
+    Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git
+fi
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 6c84a1818..c7d39c0f3 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -232,6 +232,20 @@ Section down.
   Defined.
 \end{coq_example}
 
+\subsection{\tt Cumulativity Weak Constraints}
+\optindex{Cumulativity Weak Constraints}
+
+This option, on by default, causes ``weak'' constraints to be produced
+when comparing universes in an irrelevant position. Processing weak
+constraints is delayed until minimization time. A weak constraint
+between {\tt u} and {\tt v} when neither is smaller than the other and
+one is flexible causes them to be unified. Otherwise the constraint is
+silently discarded.
+
+This heuristic is experimental and may change in future versions.
+Disabling weak constraints is more predictable but may produce
+arbitrary numbers of universes.
+
 \asection{Global and local universes}
 
 Each universe is declared in a global or local environment before it can
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index b95068ebf..bd47a04f1 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 36b6093d0..28c9dd3c2 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 6b3ce048f..9cf81ecce 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 373875bd0..e289ca169 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 b7b87370e..f6e13e1f4 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 bd9d75c6b..911799c44 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 35258762a..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
@@ -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 ef3cb91be..3b0c4bba6 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 e57afd743..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,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 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 c74467405..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)  ->
@@ -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 8e6b8f60c..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,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 -> 
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 2cbcdd76e..ba7fecadf 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -654,6 +654,11 @@ let map_with_binders g f l c0 = match kind c0 with
     let bl' = CArray.Fun1.smartmap f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
+type instance_compare_fn = global_reference -> int ->
+  Univ.Instance.t -> Univ.Instance.t -> bool
+
+type constr_compare_fn = int -> constr -> constr -> bool
+
 (* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and
    [c2] (using [k1] to expose the structure of [c1] and [k2] to expose
    the structure [c2]) using [eq] to compare the immediate subterms of
@@ -665,38 +670,42 @@ let map_with_binders g f l c0 = match kind c0 with
    optimisation that physically equal arrays are equals (hence the
    calls to {!Array.equal_norefl}). *)
 
-let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
+let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 =
   match kind1 t1, kind2 t2 with
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
   | Var id1, Var id2 -> Id.equal id1 id2
   | Sort s1, Sort s2 -> leq_sorts s1 s2
-  | Cast (c1,_,_), _ -> leq c1 t2
-  | _, Cast (c2,_,_) -> leq t1 c2
-  | Prod (_,t1,c1), Prod (_,t2,c2) -> eq t1 t2 && leq c1 c2
-  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq t1 t2 && eq c1 c2
-  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq b1 b2 && eq t1 t2 && leq c1 c2
+  | Cast (c1, _, _), _ -> leq nargs c1 t2
+  | _, Cast (c2, _, _) -> leq nargs t1 c2
+  | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2
+  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2
+  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2
   (* Why do we suddenly make a special case for Cast here? *)
-  | App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2
-  | _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2))
-  | App (c1,l1), App (c2,l2) ->
-      Int.equal (Array.length l1) (Array.length l2) &&
-        eq c1 c2 && Array.equal_norefl eq l1 l2
-  | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2
-  | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2
-  | Const (c1,u1), Const (c2,u2) -> Constant.equal c1 c2 && eq_universes true u1 u2
-  | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
-  | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2
+  | App (Cast (c1, _, _), l1), _ -> leq nargs (mkApp (c1, l1)) t2
+  | _, App (Cast (c2, _, _), l2) -> leq nargs t1 (mkApp (c2, l2))
+  | App (c1, l1), App (c2, l2) ->
+    let len = Array.length l1 in
+    Int.equal len (Array.length l2) &&
+    eq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2
+  | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2
+  | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2
+  | Const (c1,u1), Const (c2,u2) ->
+    (* The args length currently isn't used but may as well pass it. *)
+    Constant.equal c1 c2 && leq_universes (ConstRef c1) nargs u1 u2
+  | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (IndRef c1) nargs u1 u2
+  | Construct (c1,u1), Construct (c2,u2) ->
+    eq_constructor c1 c2 && leq_universes (ConstructRef c1) nargs u1 u2
   | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-      eq p1 p2 && eq c1 c2 && Array.equal eq bl1 bl2
+    eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2
   | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
-      Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
-      && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
+    Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
+    && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
+    Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
   | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _
-     | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _
-     | CoFix _), _ -> false
+    | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _
+    | CoFix _), _ -> false
 
 (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
    the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
@@ -704,8 +713,8 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
    application associativity, binders name and Cases annotations are
    not taken into account *)
 
-let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
-  compare_head_gen_leq_with kind kind  eq_universes leq_sorts eq leq t1 t2
+let compare_head_gen_leq leq_universes leq_sorts eq leq t1 t2 =
+  compare_head_gen_leq_with kind kind leq_universes leq_sorts eq leq t1 t2
 
 (* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to
    compare the immediate subterms of [c1] of [c2] if needed, [u] to
@@ -722,7 +731,7 @@ let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 =
 let compare_head_gen eq_universes eq_sorts eq t1 t2 =
   compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2
 
-let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
+let compare_head = compare_head_gen (fun _ _ -> Univ.Instance.equal) Sorts.equal
 
 (*******************************)
 (*  alpha conversion functions *)
@@ -730,41 +739,41 @@ let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
 
 (* alpha conversion : ignore print names and casts *)
 
-let rec eq_constr m n =
-  (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr m n
+let rec eq_constr nargs m n =
+  (m == n) || compare_head_gen (fun _ _ -> Instance.equal) Sorts.equal eq_constr nargs m n
 
-let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
+let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *)
 
 let eq_constr_univs univs m n =
   if m == n then true
   else 
-    let eq_universes _ = UGraph.check_eq_instances univs in
+    let eq_universes _ _ = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
-    let rec eq_constr' m n = 
-      m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
-    in compare_head_gen eq_universes eq_sorts eq_constr' m n
+    let rec eq_constr' nargs m n =
+      m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
+    in compare_head_gen eq_universes eq_sorts eq_constr' 0 m n
 
 let leq_constr_univs univs m n =
   if m == n then true
   else 
-    let eq_universes _ = UGraph.check_eq_instances univs in
+    let eq_universes _ _ = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 = s1 == s2 || 
       UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
     let leq_sorts s1 s2 = s1 == s2 || 
       UGraph.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
-    let rec eq_constr' m n = 
-      m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
+    let rec eq_constr' nargs m n =
+      m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
     in
-    let rec compare_leq m n =
-      compare_head_gen_leq 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 =
+      compare_head_gen_leq eq_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
 
 let eq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
   else 
     let cstrs = ref Constraint.empty 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
@@ -774,17 +783,17 @@ let eq_constr_univs_infer univs m n =
 	  (cstrs := Univ.enforce_eq u1 u2 !cstrs;
 	   true)
     in
-    let rec eq_constr' m n = 
-      m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
+    let rec eq_constr' nargs m n =
+      m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
     in
-    let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in
+    let res = compare_head_gen eq_universes eq_sorts eq_constr' 0 m n in
     res, !cstrs
 
 let leq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
   else 
     let cstrs = ref Constraint.empty in
-    let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in
+    let eq_universes _ _ l l' = UGraph.check_eq_instances univs l l' in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
@@ -802,19 +811,17 @@ let leq_constr_univs_infer univs m n =
 	  (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
 	   true)
     in
-    let rec eq_constr' m n = 
-      m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
+    let rec eq_constr' nargs m n =
+      m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
     in
-    let rec compare_leq m n =
-      compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
-    and leq_constr' m n = m == n || compare_leq m n in
-    let res = compare_leq m n in
+    let rec compare_leq nargs m n =
+      compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' nargs m n
+    and leq_constr' nargs m n = m == n || compare_leq nargs m n in
+    let res = compare_leq 0 m n in
     res, !cstrs
 
-let always_true _ _ = true
-
 let rec eq_constr_nounivs m n =
-  (m == n) || compare_head_gen (fun _ -> always_true) always_true eq_constr_nounivs m n
+  (m == n) || compare_head_gen (fun _ _ _ _ -> true) (fun _ _ -> true) (fun _ -> eq_constr_nounivs) 0 m n
 
 let constr_ord_int f t1 t2 =
   let (=?) f g i1 i2 j1 j2=
diff --git a/kernel/constr.mli b/kernel/constr.mli
index f7e4eecba..98c0eaa28 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -402,31 +402,38 @@ val iter : (constr -> unit) -> constr -> unit
 val iter_with_binders :
   ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
 
+type constr_compare_fn = int -> constr -> constr -> bool
+
 (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare
    the immediate subterms of [c1] of [c2] if needed; Cast's, binders
    name and Cases annotations are not taken into account *)
 
-val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
+val compare_head : constr_compare_fn -> constr_compare_fn
+
+(** Convert a global reference applied to 2 instances. The int says
+   how many arguments are given (as we can only use cumulativity for
+   fully applied inductives/constructors) .*)
+type instance_compare_fn = global_reference -> int ->
+  Univ.Instance.t -> Univ.Instance.t -> bool
 
-(** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
-   instances (the first boolean tells if they belong to a Constant.t), [s] to 
-   compare sorts; Cast's, binders name and Cases annotations are not taken 
-    into account *)
+(** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to
+   compare the immediate subterms of [c1] of [c2] if needed, [u] to
+   compare universe instances, [s] to compare sorts; Cast's, binders
+   name and Cases annotations are not taken into account *)
 
-val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+val compare_head_gen : instance_compare_fn ->
   (Sorts.t -> Sorts.t -> bool) ->
-  (constr -> constr -> bool) ->
-  constr -> constr -> bool
+  constr_compare_fn ->
+  constr_compare_fn
 
 val compare_head_gen_leq_with :
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+  instance_compare_fn ->
   (Sorts.t -> Sorts.t -> bool) ->
-  (constr -> constr -> bool) ->
-  (constr -> constr -> bool) ->
-  constr -> constr -> bool
+  constr_compare_fn ->
+  constr_compare_fn ->
+  constr_compare_fn
 
 (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2]
     like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2])
@@ -435,10 +442,10 @@ val compare_head_gen_leq_with :
 val compare_head_gen_with :
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+  instance_compare_fn ->
   (Sorts.t -> Sorts.t -> bool) ->
-  (constr -> constr -> bool) ->
-  constr -> constr -> bool
+  constr_compare_fn ->
+  constr_compare_fn
 
 (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using
     [f] to compare the immediate subterms of [c1] of [c2] for
@@ -447,11 +454,11 @@ val compare_head_gen_with :
     [s] to compare sorts for for subtyping; Cast's, binders name and
     Cases annotations are not taken into account *)
 
-val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+val compare_head_gen_leq : instance_compare_fn ->
   (Sorts.t -> Sorts.t -> bool) ->
-  (constr -> constr -> bool) ->
-  (constr -> constr -> bool) ->
-  constr -> constr -> bool
+  constr_compare_fn ->
+  constr_compare_fn ->
+  constr_compare_fn
 
 (** {6 Hashconsing} *)
 
diff --git a/kernel/names.ml b/kernel/names.ml
index 6fa44c061..a3aa71f24 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -701,6 +701,12 @@ end
 module Constrmap = Map.Make(ConstructorOrdered)
 module Constrmap_env = Map.Make(ConstructorOrdered_env)
 
+type global_reference =
+  | VarRef of variable           (** A reference to the section-context. *)
+  | ConstRef of Constant.t       (** A reference to the environment. *)
+  | IndRef of inductive          (** A reference to an inductive type. *)
+  | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
+
 (* Better to have it here that in closure, since used in grammar.cma *)
 type evaluable_global_reference =
   | EvalVarRef of Id.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 209826c1f..ffd96781b 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -500,6 +500,13 @@ val constructor_user_hash : constructor -> int
 val constructor_syntactic_ord : constructor -> constructor -> int
 val constructor_syntactic_hash : constructor -> int
 
+(** {6 Global reference is a kernel side type for all references together } *)
+type global_reference =
+  | VarRef of variable           (** A reference to the section-context. *)
+  | ConstRef of Constant.t       (** A reference to the environment. *)
+  | IndRef of inductive          (** A reference to an inductive type. *)
+  | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
+
 (** Better to have it here that in Closure, since required in grammar.cma *)
 type evaluable_global_reference =
   | EvalVarRef of Id.t
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2e59fcc18..4ecbec0ed 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -204,7 +204,8 @@ type 'a universe_compare =
   { (* Might raise NotConvertible *)
     compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a }
+    compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
+      Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a }
 
 type 'a universe_state = 'a * 'a universe_compare
 
@@ -220,12 +221,12 @@ let sort_cmp_universes env pb s0 s1 (u, check) =
 let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
 
-let get_cumulativity_constraints cv_pb cumi u u' =
+let get_cumulativity_constraints cv_pb variance u u' =
   match cv_pb with
   | CONV ->
-    Univ.ACumulativityInfo.eq_constraints cumi u u' Univ.Constraint.empty
+    Univ.enforce_eq_variance_instances variance u u' Univ.Constraint.empty
   | CUMUL ->
-    Univ.ACumulativityInfo.leq_constraints cumi u u' Univ.Constraint.empty
+    Univ.enforce_leq_variance_instances variance u u' Univ.Constraint.empty
 
 let inductive_cumulativity_arguments (mind,ind) =
   mind.Declarations.mind_nparams +
@@ -243,8 +244,7 @@ let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2
     if not (Int.equal num_param_arity nargs) then
       cmp_instances u1 u2 s
     else
-      let csts = get_cumulativity_constraints cv_pb cumi u1 u2 in
-      cmp_cumul csts s
+      cmp_cumul cv_pb (Univ.ACumulativityInfo.variance cumi) u1 u2 s
 
 let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
   convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
@@ -271,7 +271,8 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u
     else
       (** By invariant, both constructors have a common supertype,
           so they are convertible _at that type_. *)
-      s
+      let variance = Array.make (Univ.Instance.length u1) Univ.Variance.Irrelevant in
+      cmp_cumul CONV variance u1 u2 s
 
 let convert_constructors ctor nargs u1 u2 (s, check) =
   convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
@@ -678,7 +679,8 @@ let check_convert_instances ~flex u u' univs =
   else raise NotConvertible
 
 (* general conversion and inference functions *)
-let check_inductive_instances csts univs =
+let check_inductive_instances cv_pb variance u1 u2 univs =
+  let csts = get_cumulativity_constraints cv_pb variance u1 u2 in
   if (UGraph.check_constraints csts univs) then univs
   else raise NotConvertible
 
@@ -728,7 +730,8 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
     else Univ.enforce_eq_instances u u' cstrs
   in (univs, cstrs')
 
-let infer_inductive_instances csts (univs,csts') =
+let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') =
+  let csts = get_cumulativity_constraints cv_pb variance u1 u2 in
   (univs, Univ.Constraint.union csts csts')
 
 let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index ad52c93f6..14e4270b7 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -41,7 +41,8 @@ type 'a universe_compare =
   { (* Might raise NotConvertible *)
     compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a }
+    compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
+      Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a }
 
 type 'a universe_state = 'a * 'a universe_compare
 
@@ -49,7 +50,7 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 
 type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
 
-val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t ->
+val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array ->
   Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t
 
 val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
diff --git a/kernel/term.mli b/kernel/term.mli
index ba521978e..7cb3b662d 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -477,7 +477,7 @@ val iter_constr_with_binders :
   ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
 [@@ocaml.deprecated "Alias for [Constr.iter_with_binders]"]
 
-val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
+val compare_constr : (int -> constr -> constr -> bool) -> int -> constr -> constr -> bool
 [@@ocaml.deprecated "Alias for [Constr.compare_head]"]
 
 type constr = Constr.constr
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 584593e2f..be21381b7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -914,6 +914,9 @@ let enforce_eq_instances x y =
 		 (Pp.str " instances of different lengths."));
     CArray.fold_right2 enforce_eq_level ax ay
 
+let enforce_eq_variance_instances = Variance.eq_constraints
+let enforce_leq_variance_instances = Variance.leq_constraints
+
 let subst_instance_level s l =
   match l.Level.data with
   | Level.Var n -> s.(n) 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index ce617932c..629d83fb8 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -312,6 +312,9 @@ type universe_instance = Instance.t
 
 val enforce_eq_instances : Instance.t constraint_function
 
+val enforce_eq_variance_instances : Variance.t array -> Instance.t constraint_function
+val enforce_leq_variance_instances : Variance.t array -> Instance.t constraint_function
+
 type 'a puniverses = 'a * Instance.t
 val out_punivs : 'a puniverses -> 'a
 val in_punivs : 'a -> 'a puniverses
diff --git a/library/globnames.ml b/library/globnames.ml
index 8b1a51377..2fa3adba2 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -15,7 +15,7 @@ open Mod_subst
 open Libnames
 
 (*s Global reference is a kernel side type for all references together *)
-type global_reference =
+type global_reference = Names.global_reference =
   | VarRef of variable           (** A reference to the section-context. *)
   | ConstRef of Constant.t       (** A reference to the environment. *)
   | IndRef of inductive          (** A reference to an inductive type. *)
diff --git a/library/globnames.mli b/library/globnames.mli
index 017b7386d..f2b88b870 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -14,7 +14,7 @@ open Constr
 open Mod_subst
 
 (** {6 Global reference is a kernel side type for all references together } *)
-type global_reference =
+type global_reference = Names.global_reference =
   | VarRef of variable           (** A reference to the section-context. *)
   | ConstRef of Constant.t       (** A reference to the environment. *)
   | IndRef of inductive          (** A reference to an inductive type. *)
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 7d43f1986..61632e388 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -859,8 +859,9 @@ END
 
 let eq_constr x y = 
   Proofview.Goal.enter begin fun gl ->
+    let env = Tacmach.New.pf_env gl in
     let evd = Tacmach.New.project gl in
-      match EConstr.eq_constr_universes evd x y with
+      match EConstr.eq_constr_universes env evd x y with
       | Some _ -> Proofview.tclUNIT () 
       | None -> Tacticals.New.tclFAIL 0 (str "Not equal")
   end
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index fe2e86a48..d37090a65 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -352,10 +352,13 @@ let exact_ise_stack2 env evd f sk1 sk2 =
     ise_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
 
-let check_leq_inductives evd cumi u u' =
-  let u = EConstr.EInstance.kind evd u in
-  let u' = EConstr.EInstance.kind evd u' in
-  Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u')
+(* Add equality constraints for covariant/invariant positions. For
+   irrelevant positions, unify universes when flexible. *)
+let compare_cumulative_instances evd variances u u' =
+  match Evarutil.compare_cumulative_instances CONV variances u u' evd with
+  | Inl evd ->
+    Success evd
+  | Inr p -> UnifFailure (evd, UnifUnivInconsistency p)
 
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
@@ -446,103 +449,56 @@ 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 check_strict () =
-      let univs = EConstr.eq_constr_universes evd term term' in
-      match univs with
-      | Some univs ->
-        begin
-          let cstrs = Universes.to_constraints (Evd.universes evd) univs in
-          try Success (Evd.add_constraints evd cstrs)
-          with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
-        end
-      | None ->
-        UnifFailure (evd, NotSameHead)
+    let check_strict evd u u' =
+      let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in
+      try Success (Evd.add_constraints evd cstrs)
+      with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
     in
-    let first_try_strict_check cond u u' try_subtyping_constraints =
-      if cond then
-        let univs = EConstr.eq_constr_universes evd term term' in
-        match univs with
-        | Some univs ->
-          begin
-            let cstrs = Universes.to_constraints (Evd.universes evd) univs in
-            try Success (Evd.add_constraints evd cstrs)
-            with Univ.UniverseInconsistency p -> try_subtyping_constraints ()
-          end
-        | None ->
-          UnifFailure (evd, NotSameHead)
-      else
-        UnifFailure (evd, NotSameHead)
-    in
-    let compare_heads evd = 
+    let compare_heads evd =
       match EConstr.kind evd term, EConstr.kind evd term' with
-      | Const (c, u), Const (c', u') ->
-        check_strict ()
-      | Ind (ind, u), Ind (ind', u') ->
-        let check_subtyping_constraints () =
-          let nparamsaplied = Stack.args_size sk in
-          let nparamsaplied' = Stack.args_size sk' in
-          begin
-            let mind = Environ.lookup_mind (fst ind) env in
-            match mind.Declarations.mind_universes with
-            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-              UnifFailure (evd, NotSameHead)
-            | Declarations.Cumulative_ind cumi ->
-              begin
-                let num_param_arity =
-                  mind.Declarations.mind_nparams + 
-                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
-                in
-                if not (num_param_arity = nparamsaplied
-                        && num_param_arity = nparamsaplied') then
-                  UnifFailure (evd, NotSameHead)
-                else
-                  begin
-                    let evd' = check_leq_inductives evd cumi u u' in
-                    Success (check_leq_inductives evd' cumi u' u)
-                  end
-              end
+      | Const (c, u), Const (c', u') when Constant.equal c c' ->
+        let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+        check_strict evd u u'
+      | Const _, Const _ -> UnifFailure (evd, NotSameHead)
+      | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.eq_ind ind ind' ->
+        if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+        else
+          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+          let mind = Environ.lookup_mind mi env in
+          let open Declarations in
+          begin match mind.mind_universes with
+            | Monomorphic_ind _ -> assert false
+            | Polymorphic_ind _ -> check_strict evd u u'
+            | Cumulative_ind cumi ->
+              let nparamsaplied = Stack.args_size sk in
+              let nparamsaplied' = Stack.args_size sk' in
+              let needed = Reduction.inductive_cumulativity_arguments (mind,i) in
+              if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
+              then check_strict evd u u'
+              else
+                compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u'
           end
-        in
-        first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints
-      | Construct (cons, u), Construct (cons', u') ->
-        let check_subtyping_constraints () =
-          let ind, ind' = fst cons, fst cons' in
-          let j, j' = snd cons, snd cons' in
-          let nparamsaplied = Stack.args_size sk in
-          let nparamsaplied' = Stack.args_size sk' in
-          let mind = Environ.lookup_mind (fst ind) env in
-          match mind.Declarations.mind_universes with
-          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-            UnifFailure (evd, NotSameHead)
-          | Declarations.Cumulative_ind cumi ->
-            begin
-              let num_cnstr_args =
-                let nparamsctxt =
-                  mind.Declarations.mind_nparams + 
-                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
-                in
-                nparamsctxt + 
-                mind.Declarations.mind_packets.(snd ind).
-                  Declarations.mind_consnrealargs.(j - 1)
-              in
-              if not (num_cnstr_args = nparamsaplied 
-                      && num_cnstr_args = nparamsaplied') then
-                UnifFailure (evd, NotSameHead)
+      | Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
+      | Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
+        when Names.eq_constructor cons cons' ->
+        if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+        else
+          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+          let mind = Environ.lookup_mind mi env in
+          let open Declarations in
+          begin match mind.mind_universes with
+            | Monomorphic_ind _ -> assert false
+            | Polymorphic_ind _ -> check_strict evd u u'
+            | Cumulative_ind cumi ->
+              let nparamsaplied = Stack.args_size sk in
+              let nparamsaplied' = Stack.args_size sk' in
+              let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in
+              if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
+              then check_strict evd u u'
               else
-                begin
-                  (** Both constructors should be liftable to the same supertype
-                      at which we compare them, but we don't have access to that type in
-                      untyped unification. We hence try to enforce that one is lower
-                      than the other, also unifying more universes in the process.
-                      If this fails we just leave the universes as is, as in conversion. *)
-                  try Success (check_leq_inductives evd cumi u u')
-                  with Univ.UniverseInconsistency _ ->
-                    try Success (check_leq_inductives evd cumi u' u)
-                    with Univ.UniverseInconsistency e -> Success evd
-                end
-            end
-        in
-        first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints
+                Success (compare_constructor_instances evd u u')
+          end
+      | Construct _, Construct _ -> UnifFailure (evd, NotSameHead)
       | _, _ -> anomaly (Pp.str "")
     in
     ise_and evd [(fun i ->
@@ -789,7 +745,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 univs = EConstr.eq_constr_universes evd term1 term2 in
+          let univs = EConstr.eq_constr_universes env evd term1 term2 in
           match univs with
           | Some univs ->
 	      ise_and i [(fun i -> 
@@ -1096,7 +1052,7 @@ let apply_on_subterm env evdref f c t =
     (* By using eq_constr, we make an approximation, for instance, we *)
     (* could also be interested in finding a term u convertible to t *)
     (* such that c occurs in u *)
-    let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with
+    let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with
     | None -> false
     | Some cstr ->
       try ignore (Evd.add_universe_constraints !evdref cstr); true
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c9030be2d..96d80741a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1337,7 +1337,7 @@ type conv_fun_bool =
 
 let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
   let evdref = ref evd in
-  let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with
+  let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with
   | None -> false
   | Some cstr ->
     try ignore (Evd.add_universe_constraints !evdref cstr); true
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0e66ff0b6..9e3e68f05 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,6 +29,16 @@ exception Elimconst
     their parameters in its stack.
 *)
 
+let _ = Goptions.declare_bool_option {
+  Goptions.optdepr = false;
+  Goptions.optname =
+    "Generate weak constraints between Irrelevant universes";
+  Goptions.optkey = ["Cumulativity";"Weak";"Constraints"];
+  Goptions.optread = (fun () -> not !UState.drop_weak_constraints);
+  Goptions.optwrite = (fun a -> UState.drop_weak_constraints:=not a);
+}
+
+
 (** Support for reduction effects *)
 
 open Mod_subst
@@ -691,18 +701,25 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with
 let magicaly_constant_of_fixbody env sigma reference bd = function
   | Name.Anonymous -> bd
   | Name.Name id ->
+    let open Universes in
     try
       let (cst_mod,cst_sect,_) = Constant.repr3 reference in
       let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in
-      let (cst, u), ctx = Universes.fresh_constant_instance env cst in
+      let (cst, u), ctx = fresh_constant_instance env cst in
       match constant_opt_value_in env (cst,u) with
       | None -> bd
       | Some t ->
-        let csts = EConstr.eq_constr_universes sigma (EConstr.of_constr t) bd in
+        let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
         begin match csts with
         | Some csts ->
-          let subst = Universes.Constraints.fold (fun (l,d,r) acc ->
-            Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc)
+          let subst = Constraints.fold (fun cst acc ->
+              let l, r = match cst with
+                | ULub (u, v) | UWeak (u, v) -> u, v
+                | UEq (u, v) | ULe (u, v) ->
+                  let get u = Option.get (Universe.level u) in
+                  get u, get v
+              in
+            Univ.LMap.add l r acc)
             csts Univ.LMap.empty
           in
           let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
@@ -1315,10 +1332,10 @@ let sigma_compare_instances ~flex i0 i1 sigma =
      | Univ.UniverseInconsistency _ ->
 	raise Reduction.NotConvertible
 
-let sigma_check_inductive_instances csts sigma =
-  try Evd.add_constraints sigma csts
-  with Evd.UniversesDiffer
-     | Univ.UniverseInconsistency _ ->
+let sigma_check_inductive_instances cv_pb variance u1 u2 sigma =
+  match Evarutil.compare_cumulative_instances cv_pb variance u1 u2 sigma with
+  | Inl sigma -> sigma
+  | Inr _ ->
     raise Reduction.NotConvertible
 
 let sigma_univ_state = 
@@ -1334,9 +1351,9 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     let b, sigma = 
       let ans =
 	if pb == Reduction.CUMUL then 
-	  EConstr.leq_constr_universes sigma x y
+          EConstr.leq_constr_universes env sigma x y
 	else
-	  EConstr.eq_constr_universes sigma x y
+          EConstr.eq_constr_universes env sigma x y
       in
       let ans = match ans with
       | None -> None
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f4269a2c5..f2f922fd5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -561,17 +561,22 @@ let is_rigid_head sigma flags t =
     | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _)
     | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
 
-let force_eqs c = 
-  Universes.Constraints.fold
-    (fun ((l,d,r) as c) acc -> 
-      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 force_eqs c =
+  let open Universes in
+  Constraints.fold
+    (fun c acc ->
+       let c' = match c with
+         (* Should we be forcing weak constraints? *)
+         | ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r)
+         | ULe _ | UEq _ -> c
+       in
+        Constraints.add c' acc)
+    c Constraints.empty
+
+let constr_cmp pb env sigma flags t u =
   let cstrs =
-    if pb == Reduction.CONV then EConstr.eq_constr_universes sigma t u
-    else EConstr.leq_constr_universes sigma t u
+    if pb == Reduction.CONV then EConstr.eq_constr_universes env sigma t u
+    else EConstr.leq_constr_universes env sigma t u
   in 
   match cstrs with
   | Some cstrs ->
@@ -579,7 +584,7 @@ let constr_cmp pb sigma flags t u =
       with Univ.UniverseInconsistency _ -> sigma, false
       | Evd.UniversesDiffer -> 
 	if is_rigid_head sigma flags t then 
-	  try Evd.add_universe_constraints sigma (force_eqs cstrs), true
+          try Evd.add_universe_constraints sigma (force_eqs cstrs), true
 	  with Univ.UniverseInconsistency _ -> sigma, false
 	else sigma, false
       end
@@ -736,7 +741,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	| Evar (evk,_ as ev), Evar (evk',_)
             when not (Evar.Set.mem evk flags.frozen_evars)
               && Evar.equal evk evk' ->
-            let sigma',b = constr_cmp cv_pb sigma flags cM cN in
+            let sigma',b = constr_cmp cv_pb env sigma flags cM cN in
             if b then
 	      sigma',metasubst,evarsubst
             else
@@ -918,7 +923,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
   and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN =
     try canonical_projections curenvnb pb opt cM cN substn
     with ex when precatchable_exception ex ->
-    let sigma', b = constr_cmp cv_pb sigma flags cM cN in
+    let sigma', b = constr_cmp cv_pb env sigma flags cM cN in
       if b then (sigma', metas, evars)
       else
 	try reduce curenvnb pb opt substn cM cN
@@ -1087,7 +1092,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     else 
       let sigma, b = match flags.modulo_conv_on_closed_terms with
 	| Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
-	| _ -> constr_cmp cv_pb sigma flags m n in
+        | _ -> constr_cmp cv_pb env sigma flags m n in
 	if b then Some sigma
 	else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
         | Some (cv_id, cv_k), (dl_id, dl_k) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 12aef852d..b111fd1ef 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4824,9 +4824,9 @@ let intros_transitivity  n  = Tacticals.New.tclTHEN intros (transitivity_gen n)
    is solved by tac *)
 
 (** d1 is the section variable in the global context, d2 in the goal context *)
-let interpretable_as_section_decl evd d1 d2 =
+let interpretable_as_section_decl env evd d1 d2 =
   let open Context.Named.Declaration in
-  let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes !sigma c1 c2 with
+  let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with
   | None -> false
   | Some cstr ->
     try ignore (Evd.add_universe_constraints !sigma cstr); true
@@ -4890,6 +4890,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   let open Tacmach.New in
   let open Proofview.Notations in
   Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let current_sign = Global.named_context_val ()
   and global_sign = Proofview.Goal.hyps gl in
@@ -4899,7 +4900,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
       (fun d (s1,s2) ->
         let id = NamedDecl.get_id d in
 	if mem_named_context_val id current_sign &&
-          interpretable_as_section_decl evdref (lookup_named_val id current_sign) d
+          interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d
         then (s1,push_named_context_val d s2)
 	else (Context.Named.add d s1,s2))
       global_sign (Context.Named.empty, empty_named_context_val) in
diff --git a/test-suite/bugs/closed/6661.v b/test-suite/bugs/closed/6661.v
new file mode 100644
index 000000000..e88a3704d
--- /dev/null
+++ b/test-suite/bugs/closed/6661.v
@@ -0,0 +1,259 @@
+(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter" "-w" "-notation-overridden,-deprecated-option") -*- *)
+(*
+    The Coq Proof Assistant, version 8.7.1 (January 2018)
+    compiled on Jan 21 2018 15:02:24 with OCaml 4.06.0
+    from commit 391bb5e196901a3a9426295125b8d1c700ab6992
+ *)
+
+
+Require Export Coq.Init.Notations.
+Notation "'∏'  x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity) : type_scope.
+Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
+  (at level 200, x binder, y binder, right associativity).
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Reserved Notation "p @ q" (at level 60, right associativity).
+Reserved Notation "! p " (at level 50).
+
+Monomorphic Universe uu.
+Monomorphic Universe uu0.
+Monomorphic Universe uu1.
+Constraint uu0 < uu1.
+
+Global Set Universe Polymorphism.
+Global Set Polymorphic Inductive Cumulativity.
+Global Unset Universe Minimization ToSet.
+
+Notation UU  := Type (only parsing).
+Notation UU0 := Type@{uu0} (only parsing).
+
+Global Set Printing Universes.
+
+ Inductive unit : UU0 := tt : unit.
+
+Inductive paths@{i} {A:Type@{i}} (a:A) : A -> Type@{i} := idpath : paths a a.
+Hint Resolve idpath : core .
+Notation "a = b" := (paths a b) (at level 70, no associativity) : type_scope.
+
+Set Primitive Projections.
+Set Nonrecursive Elimination Schemes.
+
+Record total2@{i} { T: Type@{i} } ( P: T -> Type@{i} ) : Type@{i}
+  := tpair { pr1 : T; pr2 : P pr1 }.
+
+Arguments tpair {_} _ _ _.
+Arguments pr1 {_ _} _.
+Arguments pr2 {_ _} _.
+
+Notation "'∑'  x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..))
+  (at level 200, x binder, y binder, right associativity) : type_scope.
+
+Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X.
+  induction xy as [x y].
+  exact x.
+Defined.
+
+Unset Automatic Introduction.
+
+Definition idfun (T : UU) := λ t:T, t.
+
+Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c.
+Proof.
+  intros. induction e1. exact e2.
+Defined.
+
+Hint Resolve @pathscomp0 : pathshints.
+
+Notation "p @ q" := (pathscomp0 p q).
+
+Definition pathsinv0 {X : UU} {a b : X} (e : a = b) : b = a.
+Proof.
+  intros. induction e. exact (idpath _).
+Defined.
+
+Notation "! p " := (pathsinv0 p).
+
+Definition maponpaths {T1 T2 : UU} (f : T1 -> T2) {t1 t2 : T1}
+           (e: t1 = t2) : f t1 = f t2.
+Proof.
+  intros. induction e. exact (idpath _).
+Defined.
+
+Definition map_on_two_paths {X Y Z : UU} (f : X -> Y -> Z) {x x' y y'} (ex : x = x') (ey: y = y') :
+  f x y = f x' y'.
+Proof.
+  intros. induction ex. induction ey. exact (idpath _).
+Defined.
+
+
+Definition maponpathscomp0 {X Y : UU} {x1 x2 x3 : X}
+           (f : X -> Y) (e1 : x1 = x2) (e2 : x2 = x3) :
+  maponpaths f (e1 @ e2) = maponpaths f e1 @ maponpaths f e2.
+Proof.
+  intros. induction e1. induction e2. exact (idpath _).
+Defined.
+
+Definition maponpathsinv0 {X Y : UU} (f : X -> Y)
+           {x1 x2 : X} (e : x1 = x2) : maponpaths f (! e) = ! (maponpaths f e).
+Proof.
+  intros. induction e. exact (idpath _).
+Defined.
+
+
+
+Definition constr1 {X : UU} (P : X -> UU) {x x' : X} (e : x = x') :
+  ∑ (f : P x -> P x'),
+  ∑ (ee : ∏ p : P x, tpair _ x p = tpair _ x' (f p)),
+  ∏ (pp : P x), maponpaths pr1 (ee pp) = e.
+Proof.
+  intros. induction e.
+  split with (idfun (P x)).
+  split with (λ p, idpath _).
+  unfold maponpaths. simpl.
+  intro. exact (idpath _).
+Defined.
+
+Definition transportf@{i} {X : Type@{i}} (P : X -> Type@{i}) {x x' : X}
+           (e : x = x') : P x -> P x' := pr1 (constr1 P e).
+
+Lemma two_arg_paths_f@{i} {A : Type@{i}} {B : A -> Type@{i}} {C:Type@{i}} {f : ∏ a, B a -> C} {a1 b1 a2 b2}
+      (p : a1 = a2) (q : transportf B p b1 = b2) : f a1 b1 = f a2 b2.
+Proof.
+  intros. induction p. induction q. exact (idpath _).
+Defined.
+
+Definition iscontr@{i} (T:Type@{i}) : Type@{i} := ∑ cntr:T, ∏ t:T, t=cntr.
+
+Lemma proofirrelevancecontr {X : UU} (is : iscontr X) (x x' : X) : x = x'.
+Proof.
+  intros.
+  induction is as [y fe].
+  exact (fe x @ !(fe x')).
+Defined.
+
+
+Definition hfiber@{i} {X Y : Type@{i}} (f : X -> Y) (y : Y) : Type@{i} := total2 (λ x, f x = y).
+
+Definition hfiberpair {X Y : UU} (f : X -> Y) {y : Y}
+           (x : X) (e : f x = y) : hfiber f y :=
+  tpair _ x e.
+
+Definition coconustot (T : UU) (t : T) := ∑ t' : T, t' = t.
+
+Definition coconustotpair (T : UU) {t t' : T} (e: t' = t) : coconustot T t
+  := tpair _ t' e.
+
+Lemma connectedcoconustot {T : UU} {t : T} (c1 c2 : coconustot T t) : c1 = c2.
+Proof.
+  intros.
+  induction c1 as [x0 x].
+  induction x.
+  induction c2 as [x1 y].
+  induction y.
+  exact (idpath _).
+Defined.
+
+Definition isweq@{i} {X Y : Type@{i}} (f : X -> Y) : Type@{i} :=
+  ∏ y : Y, iscontr (hfiber f y).
+
+Lemma isProofIrrelevantUnit : ∏ x x' : unit, x = x'.
+Proof.
+  intros. induction x. induction x'. exact (idpath _).
+Defined.
+
+Lemma unitl0 : tt = tt -> coconustot _ tt.
+Proof.
+  intros e. exact (coconustotpair unit e).
+Defined.
+
+Lemma unitl1: coconustot _ tt -> tt = tt.
+Proof.
+  intro cp. induction cp as [x t]. induction x. exact t.
+Defined.
+
+Lemma unitl2: ∏ e : tt = tt, unitl1 (unitl0 e) = e.
+Proof.
+  intros. unfold unitl0. simpl. exact (idpath _).
+Defined.
+
+Lemma unitl3: ∏ e : tt = tt, e = idpath tt.
+Proof.
+  intros.
+
+  assert (e0 : unitl0 (idpath tt) = unitl0 e).
+  { simple refine (connectedcoconustot _ _). }
+
+  set (e1 := maponpaths unitl1 e0).
+
+  exact (! (unitl2 e) @ (! e1) @ (unitl2 (idpath _))).
+Defined.
+
+Theorem iscontrpathsinunit (x x' : unit) : iscontr (x = x').
+Proof.
+  intros.
+  split with (isProofIrrelevantUnit x x').
+  intros e'.
+  induction x.
+  induction x'.
+  simpl.
+  apply unitl3.
+Qed.
+
+Lemma ifcontrthenunitl0 (e1 e2 : tt = tt) : e1 = e2.
+Proof.
+  intros.
+  simple refine (proofirrelevancecontr _ _ _).
+  exact (iscontrpathsinunit tt tt).
+Qed.
+
+Section isweqcontrtounit.
+
+  Universe i.
+
+  (* To see the bug, run it both with and without this constraint: *)
+
+  (* Constraint uu0 < i. *)
+
+  (* Without this constraint, we get i = uu0 in the next definition *)
+  Lemma isweqcontrtounit@{} {T : Type@{i}} (is : iscontr@{i} T) : isweq@{i} (λ _:T, tt).
+  Proof.
+    intros. intro y. induction y.
+    induction is as [c h].
+    split with (hfiberpair@{i i i} _ c (idpath tt)).
+    intros ha.
+    induction ha as [x e].
+    simple refine (two_arg_paths_f (h x) _).
+    simple refine (ifcontrthenunitl0 _ _).
+  Defined.
+
+  (*
+     Explanation of the bug:
+
+     With the constraint uu0 < i above we get:
+
+            |= uu0 <= bug.3
+               uu0 <= i
+               uu1 <= i
+               i <= bug.3
+
+     from this print statement: *)
+
+         Print isweqcontrtounit.
+
+  (*
+
+     Without the constraint uu0 < i above we get:
+
+            |= i <= bug.3
+               uu0 = i
+
+     Since uu0 = i is not inferred when we impose the constraint uu0 < i,
+     it is invalid to infer it when we don't.
+
+   *)
+
+  Context (X : Type@{uu1}).
+
+  Check (@isweqcontrtounit X). (* detect a universe inconsistency *)
+
+End isweqcontrtounit.
diff --git a/test-suite/bugs/closed/6775.v b/test-suite/bugs/closed/6775.v
new file mode 100644
index 000000000..206df23bc
--- /dev/null
+++ b/test-suite/bugs/closed/6775.v
@@ -0,0 +1,43 @@
+(* Issue caused and fixed during the lifetime of #6775: unification
+   failing on partially applied cumulative inductives. *)
+
+Set Universe Polymorphism.
+
+Set Polymorphic Inductive Cumulativity.
+
+Unset Elimination Schemes.
+
+Inductive paths@{i} {A : Type@{i}} (a : A) : A -> Type@{i} :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Arguments inverse {A x y} p : simpl nomatch.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Arguments concat {A x y z} p q : simpl nomatch.
+
+Notation "1" := idpath.
+
+Reserved Notation "p @ q" (at level 20).
+Notation "p @ q" := (concat p q).
+
+Reserved Notation "p ^" (at level 3, format "p '^'").
+Notation "p ^" := (inverse p).
+
+Definition concat_pV_p {A} {x y z : A} (p : x = z) (q : y = z) :
+  (p @ q^) @ q = p
+  :=
+  (match q as i return forall p, (p @ i^) @ i = p with
+    idpath =>
+    fun p =>
+      match p with idpath => 1 end
+  end) p.
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index d63a3548e..034684054 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -25,7 +25,7 @@ Section ListLower.
 
 End ListLower.
 
-Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
+Lemma LowerL_Lem@{i j|j<i+} (A : Type@{j}) (l : List@{i} A) : l = LowerL@{j i} l.
 Proof. reflexivity. Qed.
 (*
 I disable these tests because cqochk can't process them when compiled with
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 4dda36042..dfa305dc6 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -10,40 +10,16 @@ Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
 
-Section ListLift.
-  Universe i j.
-
-  Constraint i < j.
-
-  Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x.
-
-End ListLift.
+Definition LiftL@{k i j|k <= i, k <= j} {A:Type@{k}} : List@{i} A -> List@{j} A := fun x => x.
 
 Lemma LiftL_Lem A (l : List A) : l = LiftL l.
 Proof. reflexivity. Qed.
 
-Section ListLower.
-  Universe i j.
-
-  Constraint i < j.
-
-  Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x.
-
-End ListLower.
-
-Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
-Proof. reflexivity. Qed.
-
 Inductive Tp := tp : Type -> Tp.
 
-Section TpLift.
-  Universe i j.
-
-  Constraint i < j.
-
-  Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x.
+Definition LiftTp@{i j|i <= j} : Tp@{i} -> Tp@{j} := fun x => x.
 
-End TpLift.
+Fail Definition LowerTp@{i j|j < i} : Tp@{i} -> Tp@{j} := fun x => x.
 
 Record Tp' := { tp' : Tp }.
 
@@ -51,22 +27,12 @@ Definition CTp := Tp.
 (* here we have to reduce a constant to infer the correct subtyping. *)
 Record Tp'' := { tp'' : CTp }.
 
-Definition LiftTp'@{i j|i < j} : Tp'@{i} -> Tp'@{j} := fun x => x.
-Definition LiftTp''@{i j|i < j} : Tp''@{i} -> Tp''@{j} := fun x => x.
+Definition LiftTp'@{i j|i <= j} : Tp'@{i} -> Tp'@{j} := fun x => x.
+Definition LiftTp''@{i j|i <= j} : Tp''@{i} -> Tp''@{j} := fun x => x.
 
 Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
 Proof. reflexivity. Qed.
 
-Section TpLower.
-  Universe i j.
-
-  Constraint i < j.
-
-  Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x.
-
-End TpLower.
-
-
 Section subtyping_test.
   Universe i j.
   Constraint i < j.
@@ -82,14 +48,8 @@ Record B (X : A) : Type := { b : X; }.
 NonCumulative Inductive NCList (A: Type)
   := ncnil | nccons : A -> NCList A -> NCList A.
 
-Section NCListLift.
-  Universe i j.
-
-  Constraint i < j.
-
-  Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x.
-
-End NCListLift.
+Fail Definition LiftNCL@{k i j|k <= i, k <= j} {A:Type@{k}}
+  : NCList@{i} A -> NCList@{j} A := fun x => x.
 
 Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
 
@@ -114,7 +74,7 @@ Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'}
   : Arrow@{i j} -> Arrow@{i' j'}
   := fun x => x.
 
-Definition arrow_lift@{i i' j j' | i' = i, j < j'}
+Definition arrow_lift@{i i' j j' | i' = i, j <= j'}
   : Arrow@{i j} -> Arrow@{i' j'}
   := fun x => x.
 
@@ -155,3 +115,16 @@ Definition checkcumul :=
 (* They can only be compared at the highest type *)
 Fail Definition checkcumul' :=
   eq_refl _ : @eq twotys@{i k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi).
+
+(* An inductive type with an irrelevant universe *)
+Inductive foo@{i} : Type@{i} := mkfoo { }.
+
+Definition bar := foo.
+
+(* The universe on mkfoo is flexible and should be unified with i. *)
+Definition foo1@{i} : foo@{i} := let x := mkfoo in x. (* fast path for conversion *)
+Definition foo2@{i} : bar@{i} := let x := mkfoo in x. (* must reduce *)
+
+(* Rigid universes however should not be unified unnecessarily. *)
+Definition foo3@{i j|} : foo@{i} := let x := mkfoo@{j} in x.
+Definition foo4@{i j|} : bar@{i} := let x := mkfoo@{j} in x.
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 4f16e1cf6..064e40b9b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1,5 +1,4 @@
 open Printf
-open Globnames
 open Libobject
 open Entries
 open Decl_kinds