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.
---
 checker/declarations.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'checker/declarations.mli')

diff --git a/checker/declarations.mli b/checker/declarations.mli
index 7458b3e0b0..ce852644ef 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -25,6 +25,9 @@ val dest_subterms : wf_paths -> wf_paths list array
 val eq_recarg : recarg -> recarg -> bool
 val eq_wf_paths : wf_paths -> wf_paths -> bool
 
+val inductive_make_projections : Names.inductive -> mutual_inductive_body ->
+  Names.Projection.Repr.t array option
+
 (* Modules *)
 
 val empty_delta_resolver : delta_resolver
-- 
cgit v1.2.3