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, 12 insertions, 15 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 6dacb7818c..fcbe939a95 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -866,22 +866,19 @@ let rec get_parameters depth n argstk =
 let eta_expand_ind_stacks env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (exp,projs) when Array.length projs > 0 
+    | Some (projs,pbs) when Array.length projs > 0 
       && mib.Declarations.mind_finite -> 
-      let primitive = Environ.is_projection projs.(0) env in
-	if primitive then
-	  (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
-	     arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
-	  let pars = mib.Declarations.mind_nparams in
-	  let right = fapp_stack (f, s') in
-	  let (depth, args, s) = strip_update_shift_app m s in
-	  (** Try to drop the params, might fail on partially applied constructors. *)
-	  let argss = try_drop_parameters depth pars args in
-	  let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
-					     term = FProj (p, right) }) projs in
-	    argss, [Zapp hstack]
-	else raise Not_found (* disallow eta-exp for non-primitive records *)
-    | _ -> raise Not_found
+	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
+	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
+      let pars = mib.Declarations.mind_nparams in
+      let right = fapp_stack (f, s') in
+      let (depth, args, s) = strip_update_shift_app m s in
+      (** Try to drop the params, might fail on partially applied constructors. *)
+      let argss = try_drop_parameters depth pars args in
+      let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
+					 term = FProj (p, right) }) projs in
+	argss, [Zapp hstack]	
+    | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with