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, 6 insertions, 0 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 34243f499c..913afb2191 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -331,6 +331,12 @@ let get_constructors env (ind,params) =
   Array.init (Array.length mip.mind_consnames)
     (fun j -> get_constructor (ind,mib,mip,params) (j+1))
 
+let get_projections env (ind,params) =
+  let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
+    match mib.mind_record with
+    | Some (projs, pbs) when Array.length projs > 0 -> Some projs
+    | _ -> None
+
 (* substitution in a signature *)
 
 let substnl_rel_context subst n sign =