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

(limited to 'kernel/environ.mli')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 0259dbbdda..f45b7be821 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -217,8 +217,11 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option
 
 (** {6 Primitive projections} *)
 
-val lookup_projection    : Names.Projection.t -> env -> projection_body
-val is_projection : Constant.t -> env -> bool
+(** Checks that the number of parameters is correct. *)
+val lookup_projection : Names.Projection.t -> env -> types
+
+val get_projection : env -> inductive -> proj_arg:int -> Names.Projection.Repr.t option
+val get_projections : env -> inductive -> Names.Projection.Repr.t array option
 
 (** {5 Inductive types } *)
 val lookup_mind_key : MutInd.t -> env -> mind_key
-- 
cgit v1.2.3