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.

5 files changed, 24 insertions, 14 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index a675fe028c..b10a4da06d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -578,7 +578,9 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
 		       constrimpls)
       impls;
   if_verbose msg_info (minductive_message names);
-  if mie.mind_entry_private == None then declare_default_schemes mind;
+  if mie.mind_entry_private == None
+    && not (mie.mind_entry_record = Some true)
+  then declare_default_schemes mind;
   mind
 
 type one_inductive_impls =
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 6f3f5cc49b..1f09d76205 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -126,7 +126,7 @@ let define internal id c p univs =
     const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff);
     const_entry_secctx = None;
     const_entry_type = None;
-    const_entry_proj = false;
+    const_entry_proj = None;
     const_entry_polymorphic = p;
     const_entry_universes = Evd.evar_context_universe_context ctx;
     const_entry_opaque = false;
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index d7d6b4c6d1..d413564a9b 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -120,7 +120,7 @@ let define id internal ctx c t =
       { const_entry_body = c;
         const_entry_secctx = None;
         const_entry_type = t;
-	const_entry_proj = false;
+	const_entry_proj = None;
 	const_entry_polymorphic = true;
 	const_entry_universes = Evd.universe_context ctx;
         const_entry_opaque = false;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 47aa2688d1..18e85266ee 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -629,7 +629,7 @@ let declare_obligation prg obl body ty uctx =
         { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff);
           const_entry_secctx = None;
 	  const_entry_type = if List.is_empty ctx then ty else None;
-	  const_entry_proj = false;
+	  const_entry_proj = None;
 	  const_entry_polymorphic = poly;
 	  const_entry_universes = uctx;
 	  const_entry_opaque = opaque;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 302fe6280e..2fbe7483f2 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -219,13 +219,13 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
   let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in
   let fields = instantiate_possibly_recursive_type indu paramdecls fields in
   let lifted_fields = Termops.lift_rel_context 1 fields in
-  let (_,kinds,sp_projs,_) =
+  let (_,_,kinds,sp_projs,_) =
     List.fold_left3
-      (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
-	let (sp_projs,subst) =
+      (fun (nfi,i,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
+	let (sp_projs,i,subst) =
 	  match fi with
 	  | Anonymous ->
-	      (None::sp_projs,NoProjection fi::subst)
+	      (None::sp_projs,i,NoProjection fi::subst)
 	  | Name fid ->
             try
               let ccl = subst_projection fid subst ti in
@@ -247,8 +247,9 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
 	      let kn =
 	        try
 		  let makeprim =
-		    if !primitive_flag && optci = None then true
-		    else false
+		    if !primitive_flag && optci = None then 
+		      Some (fst indsp, i)
+		    else None
 		  in
 		  let cie = {
                     const_entry_body =
@@ -280,12 +281,12 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
 		  let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
 		    applist (mkConstU (kn,u),proj_args) 
 	      in
-		(Some kn::sp_projs, Projection constr_fip::subst)
+		(Some kn::sp_projs, i+1, Projection constr_fip::subst)
             with NotDefinable why ->
 	      warning_or_error coe indsp why;
-	      (None::sp_projs,NoProjection fi::subst) in
-      (nfi-1,(fi, Option.is_empty optci)::kinds,sp_projs,subst))
-      (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
+	      (None::sp_projs,i,NoProjection fi::subst) in
+      (nfi-1,i,(fi, Option.is_empty optci)::kinds,sp_projs,subst))
+      (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
 let structure_signature ctx =
@@ -341,6 +342,13 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f
   let cstr = (rsp,1) in
   let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
   let build = ConstructRef cstr in
+  let () = 
+    if !primitive_flag then
+      (* declare_mutual won't have tried to define the eliminations, we do it now that 
+	 the projections have been defined. *)
+      Indschemes.declare_default_schemes kn
+    else ()
+  in
   let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
   Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
   rsp