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.

1 files changed, 5 insertions, 3 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index f76f401b4e..2c516cafd6 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -53,7 +53,8 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int;
   proj_type : types; (* Type under params *)
-  proj_body : constr; (* For compatibility, the match version *)
+  proj_eta : constr * types; (* Eta-expanded term and type *)
+  proj_body : constr; (* For compatibility with VMs only, the match version *)
 }
 
 type constant_def =
@@ -152,9 +153,10 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : (constr * constant array) option;  
+    mind_record : (constant array * projection_body array) option;  
     (** Whether the inductive type has been declared as a record, 
-	In that case we get its canonical eta-expansion and list of projections. *)
+	In the case it is primitive we get its projection names and checked
+	projection bodies, otherwise both arrays are empty. *)
 
     mind_finite : bool;  (** Whether the type is inductive or coinductive *)