Simplify even further the declaration of primitive projections,

now done entirely using declare_mind, which declares the associated
constants for primitive records. This avoids a hack related to
elimination schemes and ensures that the forward references to constants
in the mutual inductive entry are properly declared just after the
inductive. This also clarifies (and simplifies) the code of term_typing
for constants which does not have to deal with building
or checking projections anymore.
Also fix printing of universes showing the de Bruijn encoding in a few places.

1 files changed, 23 insertions, 25 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b603610ce8..a3c4d98490 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -122,6 +122,7 @@ let infer_declaration env kn dcl =
       let c = Typeops.assumption_of_judgment env j in
       let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
 	Undef nl, RegularArity t, None, poly, univs, false, ctx
+
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
 		       const_entry_polymorphic = false} as c) ->
@@ -143,6 +144,7 @@ let infer_declaration env kn dcl =
       def, RegularArity typ, None, c.const_entry_polymorphic, 
 	c.const_entry_universes,
 	c.const_entry_inline_code, c.const_entry_secctx
+
   | DefinitionEntry c ->
       let env = push_context c.const_entry_universes env in
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
@@ -152,35 +154,31 @@ let infer_declaration env kn dcl =
       let body = handle_side_effects env body side_eff in
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
-      let def, typ, proj = 
-	match c.const_entry_proj with
-	| Some (ind, i) -> (* Bind c to a checked primitive projection *)
-	  let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
-	  let kn, pb = 
-	    match mib.mind_record with
-	    | Some (kns, pbs) -> 
-	      if i < Array.length pbs then
-		kns.(i), pbs.(i)
-	      else assert false
-	    | None -> assert false
-	  in
-	  let term = Vars.subst_univs_level_constr usubst (fst pb.proj_eta) in
-	  let typ = Vars.subst_univs_level_constr usubst (snd pb.proj_eta) in
-	    Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb 
-	| None ->
-	  let j = infer env body in
-	  let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
-	  let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
-	  let def = 
-	    if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
-	    else Def (Mod_subst.from_val def) 
-	  in
-	    def, typ, None
+      let j = infer env body in
+      let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+      let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
+      let def = 
+	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
+	else Def (Mod_subst.from_val def) 
       in
 	feedback_completion_typecheck feedback_id;
-	def, typ, proj, c.const_entry_polymorphic,
+	def, typ, None, c.const_entry_polymorphic,
         univs, c.const_entry_inline_code, c.const_entry_secctx
 
+  | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
+    let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
+    let kn, pb = 
+      match mib.mind_record with
+      | Some (kns, pbs) -> 
+	if i < Array.length pbs then
+	  kns.(i), pbs.(i)
+	else assert false
+      | None -> assert false
+    in
+    let term, typ = pb.proj_eta in
+      Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
+      mib.mind_polymorphic, mib.mind_universes, false, None
+
 let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
   | TemplateArity (ctx,_) ->