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

9 files changed, 122 insertions, 85 deletions

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