From 0108db19c96e1b46346f032964f2cca3f8149cb3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 23 Jun 2018 15:38:00 +0200
Subject: Projections use index representation

The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
---
 kernel/declareops.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/declareops.mli')

diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index fb46112ea7..f91e69807f 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -66,6 +66,11 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool
 (** Is the inductive cumulative? *)
 val inductive_is_cumulative : mutual_inductive_body -> bool
 
+val inductive_make_projection : Names.inductive -> mutual_inductive_body -> proj_arg:int ->
+  Names.Projection.Repr.t option
+val inductive_make_projections : Names.inductive -> mutual_inductive_body ->
+  Names.Projection.Repr.t array option
+
 (** {6 Kernel flags} *)
 
 (** A default, safe set of flags for kernel type-checking *)
-- 
cgit v1.2.3