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.
---
 kernel/environ.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/environ.mli')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 60696184ef..344906897b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -250,6 +250,8 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option
 
 val is_primitive : env -> Constant.t -> bool
 
+val is_array_type : env -> Constant.t -> bool
+
 (** {6 Primitive projections} *)
 
 (** Checks that the number of parameters is correct. *)
-- 
cgit v1.2.3