From 32c83676c96ae4a218de0bec75d2f3353381dfb3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 28 Aug 2014 19:49:16 +0200
Subject: Change the way primitive projections are declared to the kernel.

Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.
---
 kernel/indtypes.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel/indtypes.mli')

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 8730a30457..85e6a6327a 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -41,5 +41,6 @@ val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutua
 val enforce_indices_matter : unit -> unit
 val is_indices_matter : unit -> bool
 
-val compute_expansion : pinductive -> 
-  Context.rel_context -> Context.rel_context -> (constr * constant array)
+val compute_projections : pinductive -> int -> Context.rel_context -> int array -> int array -> 
+  Context.rel_context -> 
+  (constant array * projection_body array)
-- 
cgit v1.2.3