From 89f5d2503d68dae235b9c2153d34f0def30ff626 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 12 Nov 2020 11:13:50 +0100
Subject: Make the universe of primitive arrays irrelevant

Fix #13354

This change is very specific to array, but should not be a significant
obstacle to generalization of the feature to eg axioms if we want to later.
---
 engine/eConstr.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 0c84dee572..c29de27efb 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -452,6 +452,9 @@ let eq_universes env sigma cstrs cv_pb refargs l l' =
     let open GlobRef in
     let open UnivProblem in
     match refargs with
+    | Some (ConstRef c, 1) when Environ.is_array_type env c ->
+      cstrs := compare_cumulative_instances cv_pb true [|Univ.Variance.Irrelevant|] l l' !cstrs;
+      true
     | None | Some (ConstRef _, _) ->
       cstrs := enforce_eq_instances_univs true l l' !cstrs; true
     | Some (VarRef _, _) -> assert false (* variables don't have instances *)
-- 
cgit v1.2.3