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

1 files changed, 27 insertions, 0 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6b3ce048f7..9cf81eccea 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -813,6 +813,33 @@ let subterm_source evk (loc,k) =
     | _ -> evk in
   (loc,Evar_kinds.SubEvar evk)
 
+(* Add equality constraints for covariant/invariant positions. For
+   irrelevant positions, unify universes when flexible. *)
+let compare_cumulative_instances cv_pb variances u u' sigma =
+  let open Universes in
+  let cstrs = Univ.Constraint.empty in
+  let soft = Constraints.empty in
+  let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' ->
+      let open Univ.Variance in
+      match v with
+      | Irrelevant -> cstrs, Constraints.add (UWeak (u,u')) soft
+      | Covariant when cv_pb == Reduction.CUMUL ->
+        Univ.Constraint.add (u,Univ.Le,u') cstrs, soft
+      | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft)
+      (cstrs,soft) variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+  in
+  match Evd.add_constraints sigma cstrs with
+  | sigma ->
+    Inl (Evd.add_universe_constraints sigma soft)
+  | exception Univ.UniverseInconsistency p -> Inr p
+
+let compare_constructor_instances evd u u' =
+  let open Universes in
+  let soft =
+    Array.fold_left2 (fun cs u u' -> Constraints.add (UWeak (u,u')) cs)
+      Constraints.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+  in
+  Evd.add_universe_constraints evd soft
 
 (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
     [u] up to existential variable instantiation and equalisable