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.

5 files changed, 40 insertions, 28 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index 0a06eef16..2d7b7bb0f 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -57,14 +57,13 @@ type const_entry_body = proof_output Future.computation
 
 type definition_entry = {
   const_entry_body   : const_entry_body;
-  (* List of sectoin variables *)
+  (* List of section variables *)
   const_entry_secctx : Context.section_context option;
   (* State id on which the completion of type checking is reported *)
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
   const_entry_polymorphic : bool;
   const_entry_universes   : Univ.universe_context;
-  const_entry_proj        : (mutual_inductive * int) option;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
@@ -73,9 +72,14 @@ type inline = int option (* inlining level, None for no inlining *)
 type parameter_entry = 
     Context.section_context option * bool * types Univ.in_universe_context * inline 
 
+type projection_entry = {
+  proj_entry_ind : mutual_inductive;
+  proj_entry_arg : int }
+
 type constant_entry =
   | DefinitionEntry of definition_entry
   | ParameterEntry of parameter_entry
+  | ProjectionEntry of projection_entry
 
 (** {6 Modules } *)
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 7ae787d22..759d71206 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -782,7 +782,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
     | Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 ->
       (** The elimination criterion ensures that all projections can be defined. *)
       let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in
-      let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in
+      let u = 
+	if p then 
+	  subst_univs_level_instance subst (Univ.UContext.instance ctx)
+	else Univ.Instance.empty 
+      in
 	(try 
 	   let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
 	   let kns, projs = 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b603610ce..a3c4d9849 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,_) ->
diff --git a/kernel/univ.ml b/kernel/univ.ml
index fbdb5bb0d..b2f251283 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1937,6 +1937,11 @@ let subst_univs_level_universe subst u =
   let u' = Universe.smartmap f u in
     if u == u' then u
     else Universe.sort u'
+
+let subst_univs_level_instance subst i =
+  let i' = Instance.subst_fn (subst_univs_level_level subst) i in
+    if i == i' then i
+    else i'
 	
 let subst_univs_level_constraint subst (u,d,v) =
   let u' = subst_univs_level_level subst u 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index c9b7547f2..7c0c9536f 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -374,6 +374,7 @@ val is_empty_level_subst : universe_level_subst -> bool
 val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
 val subst_univs_level_universe : universe_level_subst -> universe -> universe
 val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
+val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance
 
 (** Level to universe substitutions. *)