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.

15 files changed, 139 insertions, 99 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. *)
 
diff --git a/library/declare.ml b/library/declare.ml
index a18a6a60b..6f0ead941 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -199,7 +199,6 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types
   { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
-    const_entry_proj = None;
     const_entry_polymorphic = poly;
     const_entry_universes = univs;
     const_entry_opaque = opaque;
@@ -244,7 +243,6 @@ let declare_sideff env fix_exn se =
         const_entry_feedback = None;
 	const_entry_polymorphic = cb.const_polymorphic;
 	const_entry_universes = univs;
-	const_entry_proj = None;
     });
     cst_hyps = [] ;
     cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
@@ -391,6 +389,19 @@ let inInductive : inductive_obj -> obj =
     subst_function = ident_subst_function;
     discharge_function = discharge_inductive }
 
+let declare_projections mind =
+  let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
+    match spec.mind_record with
+    | Some (kns, pjs) -> 
+      Array.iteri (fun i kn -> 
+	let id = Label.to_id (Constant.label kn) in
+	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
+	let kn' = declare_constant id (ProjectionEntry entry,
+				       IsDefinition StructureComponent) 
+	in
+	  assert(eq_constant kn kn')) kns
+    | None -> ()
+
 (* for initial declaration *)
 let declare_mind isrecord mie =
   let id = match mie.mind_entry_inds with
@@ -398,6 +409,7 @@ let declare_mind isrecord mie =
     | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
   let mind = Global.mind_of_delta_kn kn in
+  declare_projections mind;
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
   if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname);
diff --git a/library/global.ml b/library/global.ml
index 65e895dfd..adfb7cafe 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -152,7 +152,9 @@ let type_of_global_unsafe r =
   | VarRef id -> Environ.named_type id env
   | ConstRef c -> 
      let cb = Environ.lookup_constant c env in 
-       Typeops.type_of_constant_type env cb.Declarations.const_type
+     let univs = Declareops.universes_of_polymorphic_constant cb in
+     let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in
+       Vars.subst_instance_constr (Univ.UContext.instance univs) ty
   | IndRef ind ->
      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
      let inst = 
@@ -195,7 +197,7 @@ let universes_of_global env r =
     | VarRef id -> Univ.UContext.empty
     | ConstRef c -> 
       let cb = Environ.lookup_constant c env in 
-	Declareops.universes_of_constant cb
+	Declareops.universes_of_polymorphic_constant cb
     | IndRef ind ->
       let (mib, oib) = Inductive.lookup_mind_specif env ind in
 	Univ.instantiate_univ_context mib.mind_universes 
diff --git a/printing/printer.ml b/printing/printer.ml
index 55a7d36a3..ed872afc6 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -778,7 +778,7 @@ let print_mutual_inductive env mind mib =
     str (if mib.mind_finite then "Inductive " else "CoInductive ") ++
     prlist_with_sep (fun () -> fnl () ++ str"  with ")
       (print_one_inductive env mib) inds ++
-      pr_universe_ctx mib.mind_universes)
+      pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
 
 let get_fields =
   let rec prodec_rec l subst c =
@@ -820,7 +820,7 @@ let print_record env mind mib =
         (fun (id,b,c) ->
 	  pr_id id ++ str (if b then " : " else " := ") ++
 	  pr_lconstr_env envpar c) fields) ++ str" }" ++
-      pr_universe_ctx mib.mind_universes)
+      pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
 
 let pr_mutual_inductive_body env mind mib =
   if mib.mind_record <> None && not !Flags.raw_print then
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index b619eafab..82e176f97 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -316,8 +316,7 @@ let close_proof ?feedback_id ~now fpl =
 	  const_entry_inline_code = false;
 	  const_entry_opaque = true;
 	  const_entry_universes = univs;
-	  const_entry_polymorphic = poly;
-	  const_entry_proj = None})
+	  const_entry_polymorphic = poly})
       fpl initial_goals in
   { id = pid; entries = entries; persistence = strength; universes = universes },
   Ephemeron.get terminator
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
new file mode 100644
index 000000000..2682df3b7
--- /dev/null
+++ b/test-suite/success/primitiveproj.v
@@ -0,0 +1,30 @@
+Set Primitive Projections.
+Set Record Elimination Schemes.
+Module Prim.
+
+Record F := { a : nat; b : a = a }.
+Record G (A : Type) := { c : A; d : F }.
+
+Check c.
+End Prim.
+Module Univ.
+Set Universe Polymorphism.
+Set Implicit Arguments.
+Record Foo (A : Type) := { foo : A }.
+
+Record G (A : Type) := { c : A; d : c = c; e : Foo A }.
+
+Definition Foon : Foo nat := {| foo := 0 |}.
+
+Definition Foonp : nat := Foon.(foo).
+
+Definition Gt : G nat := {| c:= 0; d:=eq_refl; e:= Foon |}.
+
+Check (Gt.(e)).
+
+Section bla.
+
+  Record bar := { baz : nat; def := 0; baz' : forall x, x = baz \/ x = def }.
+End bla.
+
+End Univ.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 69c0aaea8..d7c96feca 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -592,7 +592,6 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
       impls;
   if_verbose msg_info (minductive_message names);
   if mie.mind_entry_private == None
-    && not (mie.mind_entry_record = Some true)
   then declare_default_schemes mind;
   mind
 
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 1f09d7620..8dcb32442 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -126,7 +126,6 @@ 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 = 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 d413564a9..b422e67b1 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -120,7 +120,6 @@ let define id internal ctx c t =
       { const_entry_body = c;
         const_entry_secctx = None;
         const_entry_type = t;
-	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 18e85266e..9694c2d7f 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -629,7 +629,6 @@ 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 = None;
 	  const_entry_polymorphic = poly;
 	  const_entry_universes = uctx;
 	  const_entry_opaque = opaque;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e46a29ba8..fedf63eed 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -240,64 +240,60 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
 	  match fi with
 	  | Anonymous ->
 	      (None::sp_projs,i,NoProjection fi::subst)
-	  | Name fid ->
-            try
-              let ccl = subst_projection fid subst ti in
-	      let body = match optci with
-              | Some ci -> subst_projection fid subst ci
-              | None ->
-	        (* [ccl] is defined in context [params;x:rp] *)
-		(* [ccl'] is defined in context [params;x:rp;x:rp] *)
-		let ccl' = liftn 1 2 ccl in
-		let p = mkLambda (x, lift 1 rp, ccl') in
-		let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
-		let ci = Inductiveops.make_case_info env indsp LetStyle in
-		  mkCase (ci, p, mkRel 1, [|branch|]) 
-	      in
-	      let proj =
-	        it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
-              let projtyp =
-                it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
-	      let kn =
+	  | Name fid -> try
+	    let kn, term = 
+	      if optci = None && primitive then 
+		  (** Already defined in the kernel silently *)
+		let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in
+		  Declare.definition_message fid;
+		  kn, mkProj (kn,mkRel 1)
+	      else
+		let ccl = subst_projection fid subst ti in
+		let body = match optci with
+		  | Some ci -> subst_projection fid subst ci
+		  | None ->
+	            (* [ccl] is defined in context [params;x:rp] *)
+		    (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+		    let ccl' = liftn 1 2 ccl in
+		    let p = mkLambda (x, lift 1 rp, ccl') in
+		    let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
+		    let ci = Inductiveops.make_case_info env indsp LetStyle in
+		      mkCase (ci, p, mkRel 1, [|branch|]) 
+		in
+		let proj =
+	          it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
+		let projtyp =
+                  it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
 	        try
-		  let makeprim =
-		    if primitive && optci = None then 
-		      Some (fst indsp, i)
-		    else None
-		  in
-		  let cie = {
-                    const_entry_body =
-                      Future.from_val (Term_typing.mk_pure_proof proj);
-                    const_entry_secctx = None;
-                    const_entry_type = Some projtyp;
+		  let entry = {
+		    const_entry_body =
+		      Future.from_val (Term_typing.mk_pure_proof proj);
+		    const_entry_secctx = None;
+		    const_entry_type = Some projtyp;
 		    const_entry_polymorphic = poly;
 		    const_entry_universes = ctx;
-		    const_entry_proj = makeprim;
-                    const_entry_opaque = false;
-                    const_entry_inline_code = false;
-                    const_entry_feedback = None;
-                  } in
-		  let k = (DefinitionEntry cie,IsDefinition kind) in
+		    const_entry_opaque = false;
+		    const_entry_inline_code = false;
+		    const_entry_feedback = None } in
+		  let k = (DefinitionEntry entry,IsDefinition kind) in
 		  let kn = declare_constant ~internal:KernelSilent fid k in
-		  Declare.definition_message fid;
-		  kn
+		  let constr_fip =
+		    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
+		      applist (mkConstU (kn,u),proj_args) 
+		  in
+		    Declare.definition_message fid;
+		    kn, constr_fip
                 with Type_errors.TypeError (ctx,te) ->
-                  raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
-	      let refi = ConstRef kn in
-	      Impargs.maybe_declare_manual_implicits false refi impls;
-	      if coe then begin
-	        let cl = Class.class_of_global (IndRef indsp) in
+                  raise (NotDefinable (BadTypedProj (fid,ctx,te))) 
+	    in
+	    let refi = ConstRef kn in
+	    Impargs.maybe_declare_manual_implicits false refi impls;
+	    if coe then begin
+	      let cl = Class.class_of_global (IndRef indsp) in
 	        Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
-	      end;
-	      let constr_fip =
-		if primitive then mkProj (kn,mkRel 1)
-		else
-		  let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
-		    applist (mkConstU (kn,u),proj_args) 
-	      in
-	      let i = if Option.is_empty optci then i+1 else i in
-		(Some kn::sp_projs, i,
-		  Projection constr_fip::subst)
+	    end;
+	    let i = if Option.is_empty optci then i+1 else i in
+	      (Some kn::sp_projs, i, Projection term::subst)
             with NotDefinable why ->
 	      warning_or_error coe indsp why;
 	      (None::sp_projs,i,NoProjection fi::subst) in
@@ -358,13 +354,6 @@ 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