From 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 16 Feb 2018 15:44:44 +0100
Subject: Allow using cumulativity without forcing strict constraints.

Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative
inductive would try to generate a constraint [i = j] and use
cumulativity only if this resulted in an inconsistency. This is
confusingly different from the behaviour with [Type] and means
cumulativity can only be used to lift between universes related by
strict inequalities. (This isn't a kernel restriction so there might
be some workaround to send the kernel the right constraints, but
not in a nice way.)

See modified test for more details of what is now possible.

Technical notes:

When universe constraints were inferred by comparing the shape of
terms without reduction, cumulativity was not used and so too-strict
equality constraints were generated. Then in order to use cumulativity
we had to make this comparison fail to fall back to full conversion.

When unifiying 2 instances of a cumulative inductive type, if there
are any Irrelevant universes we try to unify them if they are
flexible.
---
 engine/eConstr.ml                 | 133 ++++++++++++++------
 engine/eConstr.mli                |   7 +-
 engine/termops.ml                 |  14 +--
 engine/termops.mli                |   2 -
 engine/universes.ml               |  41 +-----
 engine/universes.mli              |   4 -
 kernel/constr.ml                  | 113 +++++++++--------
 kernel/constr.mli                 |  47 ++++---
 kernel/names.ml                   |   6 +
 kernel/names.mli                  |   7 ++
 kernel/term.mli                   |   2 +-
 library/globnames.ml              |   2 +-
 library/globnames.mli             |   2 +-
 plugins/ltac/extratactics.ml4     |   3 +-
 pretyping/evarconv.ml             | 175 +++++++++++---------------
 pretyping/evarsolve.ml            |   2 +-
 pretyping/reductionops.ml         |   6 +-
 pretyping/unification.ml          |  12 +-
 tactics/tactics.ml                |   7 +-
 test-suite/bugs/closed/6661.v     | 259 ++++++++++++++++++++++++++++++++++++++
 test-suite/bugs/closed/6775.v     |  43 +++++++
 test-suite/coqchk/cumulativity.v  |   2 +-
 test-suite/success/cumulativity.v |  56 ++-------
 vernac/obligations.ml             |   1 -
 24 files changed, 616 insertions(+), 330 deletions(-)
 create mode 100644 test-suite/bugs/closed/6661.v
 create mode 100644 test-suite/bugs/closed/6775.v

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index b95068ebf..59dc5a221 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -548,39 +548,100 @@ 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
+         let u = Univ.Universe.make u in
+         let u' = Univ.Universe.make u' in
+         match v with
+         | Irrelevant -> Constraints.add (u,ULub,u') cstrs
+         | Covariant ->
+           (match cv_pb with
+            | Reduction.CONV -> Constraints.add (u,UEq,u') cstrs
+            | Reduction.CUMUL -> Constraints.add (u,ULe,u') cstrs)
+         | Invariant -> Constraints.add (u,UEq,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
+    let variances = Univ.ACumulativityInfo.variance cumi in
+    compare_cumulative_instances Reduction.CONV (Int.equal num_cnstr_args nargs) variances u1 u2 cstrs
+
+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
@@ -597,24 +658,25 @@ let test_constr_universes sigma leq m n =
 	   (Sorts.univ_of_sort s1,ULe,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 +686,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;
 	 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/termops.ml b/engine/termops.ml
index 35258762a..20b6b3504 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -914,12 +914,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 +933,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/universes.ml b/engine/universes.ml
index c74467405..70ed6311e 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -242,7 +242,7 @@ 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
@@ -251,45 +251,12 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
       | 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
 
diff --git a/engine/universes.mli b/engine/universes.mli
index 8e6b8f60c..a86b9779b 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -102,10 +102,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. *)
 
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/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/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..130aa8cd7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -352,10 +352,34 @@ 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')
+let try_soft evd u u' =
+  let open Universes in
+  let make = Univ.Universe.make in
+  try Evd.add_universe_constraints evd (Constraints.singleton (make u,ULub,make u'))
+  with UState.UniversesDiffer | Univ.UniverseInconsistency _ -> evd
+
+(* Add equality constraints for covariant/invariant positions. For
+   irrelevant positions, unify universes when flexible. *)
+let compare_cumulative_instances evd variances u u' =
+  let cstrs = Univ.Constraint.empty in
+  let soft = [] in
+  let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' ->
+      let open Univ.Variance in
+      match v with
+      | Irrelevant -> cstrs, (u,u')::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 evd cstrs with
+  | evd ->
+    Success (List.fold_left (fun evd (u,u') -> try_soft evd u u') evd soft)
+  | exception Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
+
+(* We should only compare constructors at convertible types, so this
+   is only an opportunity to unify universes. *)
+let compare_constructor_instances evd u u' =
+  Array.fold_left2 try_soft
+    evd (Univ.Instance.to_array u) (Univ.Instance.to_array u')
 
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
@@ -446,103 +470,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 +766,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 +1073,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 44a69d1c1..0a28f1fb8 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -698,7 +698,7 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
       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 ->
@@ -1332,9 +1332,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..1cd8d3940 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -568,10 +568,10 @@ let force_eqs c =
 	Universes.Constraints.add c' acc) 
     c Universes.Constraints.empty
 
-let constr_cmp pb sigma flags t u =
+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 ->
@@ -736,7 +736,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 +918,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 +1087,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..5f4500715 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 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..0394ea340 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.
+Definition LiftTp@{i j|i <= j} : Tp@{i} -> Tp@{j} := fun x => x.
 
-  Constraint i < j.
-
-  Definition LiftTp : 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.
 
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
-- 
cgit v1.2.3