Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).

14 files changed, 315 insertions, 156 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 4bae6de66..3d580d713 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -183,21 +183,17 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
     Context.fold_named_context (fun (h,_,_) hyps ->
       List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps)
       hyps ~init:cb.const_hyps in
-
-  (* let typ = match cb.const_type with *)
-  (*   | NonPolymorphicType t -> *)
-  (* 	let typ = *)
-  (*         abstract_constant_type (expmod_constr cache r.d_modlist t) hyps in *)
-  (* 	NonPolymorphicType typ *)
-  (*   | PolymorphicArity (ctx,s) -> *)
-  (* 	let t = mkArity (ctx,Type s.poly_level) in *)
-  (* 	let typ = *)
-  (*         abstract_constant_type (expmod_constr cache r.d_modlist t) hyps in *)
-  (* 	let j = make_judge (constr_of_def body) typ in *)
-  (* 	Typeops.make_polymorphic_if_constant_for_ind env j *)
-  (* in *)
-  let typ = 
-    abstract_constant_type (expmod_constr cache modlist cb.const_type) hyps 
+  let typ = match cb.const_type with
+    | RegularArity t ->
+  	let typ =
+          abstract_constant_type (expmod_constr cache modlist t) hyps in
+  	RegularArity typ
+    | TemplateArity (ctx,s) ->
+  	let t = mkArity (ctx,Type s.template_level) in
+  	let typ =
+          abstract_constant_type (expmod_constr cache modlist t) hyps in
+  	let j = make_judge (constr_of_def body) typ in
+  	Typeops.make_polymorphic_if_constant_for_ind env j
   in
   let projection pb =
     let c' = abstract_constant_body (expmod_constr cache modlist pb.proj_body) hyps in
@@ -210,6 +206,9 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
 	  | _ -> assert false 
       with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0)
     in 
+    let typ = (* By invariant, a regular arity *)
+      match typ with RegularArity t -> t | TemplateArity _ -> assert false 
+    in
     let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in
       { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
 	proj_type = ty'; proj_body = c' }
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index f3cb41f32..f269e165e 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -18,7 +18,24 @@ type engagement = ImpredicativeSet
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
-type constant_type = types
+(** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives
+    and constants hiding inductives are implicitely polymorphic when
+    applied to parameters, on the universes appearing in the whnf of
+    their parameters and their conclusion, in a template style.
+    
+    In truely universe polymorphic mode, we always use RegularArity.
+*)
+
+type template_arity = {
+  template_param_levels : Univ.universe option list;
+  template_level : Univ.universe;
+}
+
+type ('a, 'b) declaration_arity = 
+  | RegularArity of 'a
+  | TemplateArity of 'b
+
+type constant_type = (types, rel_context * template_arity) declaration_arity
 
 (** Inlining level of parameters at functor applications.
     None means no inlining *)
@@ -79,11 +96,13 @@ type wf_paths = recarg Rtree.t
 v}
 *)
 
-type inductive_arity = {
+type regular_inductive_arity = {
   mind_user_arity : types;
   mind_sort : sorts;
 }
 
+type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity
+
 type one_inductive_body = {
 (** {8 Primitive datas } *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 0e4b80495..be6c18810 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -13,6 +13,28 @@ open Util
 (** Operations concernings types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
 
+(** {6 Arities } *)
+
+let subst_decl_arity f g sub ar = 
+  match ar with
+  | RegularArity x -> 
+    let x' = f sub x in 
+      if x' == x then ar
+      else RegularArity x'
+  | TemplateArity x -> 
+    let x' = g sub x in 
+      if x' == x then ar
+      else TemplateArity x'
+
+let map_decl_arity f g = function
+  | RegularArity a -> RegularArity (f a)
+  | TemplateArity a -> TemplateArity (g a)
+
+let hcons_template_arity ar =
+  { template_param_levels =
+      List.smartmap (Option.smartmap Univ.hcons_univ) ar.template_param_levels;
+    template_level = Univ.hcons_univ ar.template_level }
+
 (** {6 Constants } *)
 
 let body_of_constant cb = match cb.const_body with
@@ -44,14 +66,10 @@ let subst_rel_declaration sub (id,copt,t as x) =
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
-(* let subst_const_type sub arity = match arity with *)
-(*   | NonPolymorphicType s -> *)
-(*     let s' = subst_mps sub s in *)
-(*     if s==s' then arity else NonPolymorphicType s' *)
-(*   | PolymorphicArity (ctx,s) -> *)
-(*     let ctx' = subst_rel_context sub ctx in *)
-(*     if ctx==ctx' then arity else PolymorphicArity (ctx',s) *)
-
+let subst_template_cst_arity sub (ctx,s as arity) =
+  let ctx' = subst_rel_context sub ctx in
+    if ctx==ctx' then arity else (ctx',s)
+      
 let subst_const_type sub arity =
   if is_empty_subst sub then arity
   else subst_mps sub arity
@@ -73,7 +91,7 @@ let subst_const_body sub cb =
   if is_empty_subst sub then cb
   else
     let body' = subst_const_def sub cb.const_body in
-    let type' = subst_const_type sub cb.const_type in
+    let type' = subst_decl_arity subst_const_type subst_template_cst_arity sub cb.const_type in
     let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in
     if body' == cb.const_body && type' == cb.const_type
       && proj' == cb.const_proj then cb
@@ -102,7 +120,13 @@ let hcons_rel_decl ((n,oc,t) as d) =
 
 let hcons_rel_context l = List.smartmap hcons_rel_decl l
 
-let hcons_const_type t = Term.hcons_constr t
+let hcons_regular_const_arity t = Term.hcons_constr t
+
+let hcons_template_const_arity (ctx, ar) = 
+  (hcons_rel_context ctx, hcons_template_arity ar)
+
+let hcons_const_type = 
+  map_decl_arity hcons_regular_const_arity hcons_template_const_arity
 
 let hcons_const_def = function
   | Undef inl -> Undef inl
@@ -164,72 +188,15 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
 
 (** {7 Substitution of inductive declarations } *)
 
-(* OLD POLYMORPHISM *)
-(* let subst_indarity sub ar = match ar with *)
-(*   | Monomorphic s -> *)
-(*     let uar' = subst_mps sub s.mind_user_arity in *)
-(*     if uar' == s.mind_user_arity then ar *)
-(*     else Monomorphic { mind_user_arity = uar'; mind_sort = s.mind_sort } *)
-(*   | Polymorphic _ -> ar *)
-
-(* let subst_mind_packet sub mip = *)
-(*   let { mind_nf_lc = nf; *)
-(*         mind_user_lc = user; *)
-(*         mind_arity_ctxt = ctxt; *)
-(*         mind_arity = ar; *)
-(*         mind_recargs = ra } = mip *)
-(*   in *)
-(*   let nf' = Array.smartmap (subst_mps sub) nf in *)
-(*   let user' = *)
-(*     (\* maintain sharing of [mind_user_lc] and [mind_nf_lc] *\) *)
-(*     if user==nf then nf' *)
-(*     else Array.smartmap (subst_mps sub) user *)
-(*   in *)
-(*   let ctxt' = subst_rel_context sub ctxt in *)
-(*   let ar' = subst_indarity sub ar in *)
-(*   let ra' = subst_wf_paths sub ra in *)
-(*   if nf==nf' && user==user' && ctxt==ctxt' && ar==ar' && ra==ra' *)
-(*   then mip *)
-(*   else *)
-(*     { mip with *)
-(*       mind_nf_lc = nf'; *)
-(*       mind_user_lc = user'; *)
-(*       mind_arity_ctxt = ctxt'; *)
-(*       mind_arity = ar'; *)
-(*       mind_recargs = ra' } *)
-
-(* let subst_mind sub mib = *)
-(*   assert (List.is_empty mib.mind_hyps); (\* we're outside sections *\) *)
-(*   if is_empty_subst sub then mib *)
-(*   else *)
-(*     let params = mib.mind_params_ctxt in *)
-(*     let params' = Context.map_rel_context (subst_mps sub) params in *)
-(*     let packets = mib.mind_packets in *)
-(*     let packets' = Array.smartmap (subst_mind_packet sub) packets in *)
-(*     if params==params' && packets==packets' then mib *)
-(*     else *)
-(*       { mib with *)
-(*         mind_params_ctxt = params'; *)
-(*         mind_packets = packets'; *)
-(*         mind_native_name = ref NotLinked } *)
-
-(* (\** {6 Hash-consing of inductive declarations } *\) *)
-
-(* (\** Just as for constants, this hash-consing is quite partial *\) *)
-
-(* let hcons_indarity = function *)
-(*   | Monomorphic a -> *)
-(*     Monomorphic *)
-(*       { mind_user_arity = Term.hcons_constr a.mind_user_arity; *)
-(*         mind_sort = Term.hcons_sorts a.mind_sort } *)
-(*   | Polymorphic a -> Polymorphic (hcons_polyarity a) *)
+let subst_regular_ind_arity sub s =
+  let uar' = subst_mps sub s.mind_user_arity in
+    if uar' == s.mind_user_arity then s 
+    else { mind_user_arity = uar'; mind_sort = s.mind_sort }
 
-(** Substitution of inductive declarations *)
+let subst_template_ind_arity sub s = s
 
-let subst_indarity sub s =
-  { mind_user_arity = subst_mps sub s.mind_user_arity;
-    mind_sort = s.mind_sort;
-  }
+let subst_ind_arity =
+  subst_decl_arity subst_regular_ind_arity subst_template_ind_arity
 
 let subst_mind_packet sub mbp =
   { mind_consnames = mbp.mind_consnames;
@@ -238,7 +205,7 @@ let subst_mind_packet sub mbp =
     mind_typename = mbp.mind_typename;
     mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
     mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
-    mind_arity = subst_indarity sub mbp.mind_arity;
+    mind_arity = subst_ind_arity sub mbp.mind_arity;
     mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
     mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
@@ -261,12 +228,19 @@ let subst_mind_body sub mib =
     mind_polymorphic = mib.mind_polymorphic;
     mind_universes = mib.mind_universes }
 
-(** Hash-consing of inductive declarations *)
+(** {6 Hash-consing of inductive declarations } *)
 
-let hcons_indarity a =
+let hcons_regular_ind_arity a =
   { mind_user_arity = Term.hcons_constr a.mind_user_arity;
     mind_sort = Term.hcons_sorts a.mind_sort }
 
+(** Just as for constants, this hash-consing is quite partial *)
+
+let hcons_ind_arity =
+  map_decl_arity hcons_regular_ind_arity hcons_template_arity
+
+(** Substitution of inductive declarations *)
+
 let hcons_mind_packet oib =
   let user = Array.smartmap Term.hcons_types oib.mind_user_lc in
   let nf = Array.smartmap Term.hcons_types oib.mind_nf_lc in
@@ -275,7 +249,7 @@ let hcons_mind_packet oib =
   { oib with
     mind_typename = Names.Id.hcons oib.mind_typename;
     mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
-    mind_arity = hcons_indarity oib.mind_arity;
+    mind_arity = hcons_ind_arity oib.mind_arity;
     mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames;
     mind_user_lc = user;
     mind_nf_lc = nf }
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 0c5f3584e..9f5197668 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -12,6 +12,11 @@ open Mod_subst
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
 
+(** {6 Arities} *)
+
+val map_decl_arity : ('a -> 'c) -> ('b -> 'd) ->
+  ('a, 'b) declaration_arity -> ('c, 'd) declaration_arity
+
 (** {6 Constants} *)
 
 val subst_const_body : substitution -> constant_body -> constant_body
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 323d6fcea..1f29fd67a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -214,12 +214,22 @@ let universes_and_subst_of cb u =
   let subst = Univ.make_universe_subst u univs in
     subst, Univ.instantiate_univ_context subst univs
 
+let get_regular_arity = function
+  | RegularArity a -> a
+  | TemplateArity _ -> assert false
+
+let map_regular_arity f = function
+  | RegularArity a as ar -> 
+    let a' = f a in 
+      if a' == a then ar else RegularArity a'
+  | TemplateArity _ -> assert false
+
 (* constant_type gives the type of a constant *)
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
       let subst, csts = universes_and_subst_of cb u in
-	(subst_univs_constr subst cb.const_type, csts)
+	(map_regular_arity (subst_univs_constr subst) cb.const_type, csts)
     else cb.const_type, Univ.Constraint.empty
 
 let constant_type_in_ctx env kn =
@@ -260,7 +270,8 @@ let constant_value_and_type env (kn, u) =
 	| Def l_body -> Some (subst_univs_constr subst (Mod_subst.force_constr l_body))
 	| OpaqueDef _ -> None
 	| Undef _ -> None
-      in b', subst_univs_constr subst cb.const_type, cst
+      in
+	b', map_regular_arity (subst_univs_constr subst) cb.const_type, cst
     else 
       let b' = match cb.const_body with
 	| Def l_body -> Some (Mod_subst.force_constr l_body)
@@ -277,7 +288,7 @@ let constant_type_in env (kn,u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
       let subst = Univ.make_universe_subst u (Future.force cb.const_universes) in
-	subst_univs_constr subst cb.const_type
+	map_regular_arity (subst_univs_constr subst) cb.const_type
     else cb.const_type
 
 let constant_value_in env (kn,u) =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index fb5d79718..330d9c277 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -140,12 +140,12 @@ type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
 
 val constant_value : env -> constant puniverses -> constr constrained
-val constant_type : env -> constant puniverses -> types constrained
-val constant_type_in_ctx : env -> constant -> types Univ.in_universe_context
+val constant_type : env -> constant puniverses -> constant_type constrained
+val constant_type_in_ctx : env -> constant -> constant_type Univ.in_universe_context
 
 val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option
 val constant_value_and_type : env -> constant puniverses -> 
-  types option * constr * Univ.constraints
+  constr option * constant_type * Univ.constraints
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
 val constant_context : env -> constant -> Univ.universe_context
@@ -154,7 +154,7 @@ val constant_context : env -> constant -> Univ.universe_context
    already contains the constraints corresponding to the constant 
    application. *)
 val constant_value_in : env -> constant puniverses -> constr
-val constant_type_in : env -> constant puniverses -> types
+val constant_type_in : env -> constant puniverses -> constant_type
 val constant_opt_value_in : env -> constant puniverses -> constr option
 
 
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index b441e02a3..8b7230c3b 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -109,17 +109,40 @@ let check_hyps_inclusion env f c sign =
 
 (* Type of constants *)
 
-let type_of_constant env cst = constant_type env cst
-let type_of_constant_in env cst = constant_type_in env cst
-let type_of_constant_knowing_parameters env t _ = t
 
-let judge_of_constant env (kn,u as cst) =
+let type_of_constant_knowing_parameters_arity env t paramtyps =
+  match t with
+  | RegularArity t -> t
+  | TemplateArity (sign,ar) ->
+      let ctx = List.rev sign in
+      let ctx,s = instantiate_universes env ctx ar paramtyps in
+      mkArity (List.rev ctx,s)
+
+let type_of_constant_knowing_parameters env cst paramtyps =
+  let ty, cu = constant_type env cst in
+    type_of_constant_knowing_parameters_arity env ty paramtyps, cu
+
+let type_of_constant_type env t =
+  type_of_constant_knowing_parameters_arity env t [||]
+
+let type_of_constant env cst =
+  type_of_constant_knowing_parameters env cst [||]
+
+let type_of_constant_in env cst =
+  let ar = constant_type_in env cst in
+    type_of_constant_knowing_parameters_arity env ar [||]
+
+let judge_of_constant_knowing_parameters env (kn,u as cst) jl =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
-  let ty, cu = type_of_constant env cst in
+  let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
+  let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
   let () = check_constraints cu env in
     ty
 
+let judge_of_constant env cst =
+  judge_of_constant_knowing_parameters env cst [||]
+
 let type_of_projection env (cst,u) =
   let cb = lookup_constant cst env in
   match cb.const_proj with
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0ac6a4e4a..e89bbf0d9 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -300,7 +300,7 @@ let typecheck_inductive env ctx mie =
 	     Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is "
 	     ++ Universe.pr infu)
       in
-	(id,cn,lc,(sign,(not is_natural,full_arity,defu))))
+	(id,cn,lc,(sign,RegularArity (not is_natural,full_arity,defu))))
     inds
   in (env_arities, params, inds)
 
@@ -615,9 +615,13 @@ let allowed_sorts is_smashed s =
 (* - all_sorts in case of small, unitary Prop (not smashed) *)
 (* - logical_sorts in case of large, unitary Prop (smashed) *)
 
+let arity_conclusion = function
+  | RegularArity (_, c, _) -> c
+  | TemplateArity s -> mkType s.template_level
+
 let fold_inductive_blocks f =
   Array.fold_left (fun acc (_,_,lc,(arsign,ar)) ->
-    f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (pi2 ar) arsign))
+    f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (arity_conclusion ar) arsign))
 
 let used_section_variables env inds =
   let ids = fold_inductive_blocks
@@ -675,12 +679,14 @@ let build_inductive env p ctx env_ar params kn isrecord isfinite inds nmr recarg
 	splayed_lc in
     (* Elimination sorts *)
     let arkind,kelim = 
-      let (info,ar,defs) = ar_kind in
-      let s = sort_of_univ defs in
-      let kelim = allowed_sorts info s in
-	{ mind_user_arity = ar;
-	  mind_sort = s;
-	}, kelim in
+      match ar_kind with
+      | TemplateArity ar -> TemplateArity ar, all_sorts
+      | RegularArity (info,ar,defs) ->
+	let s = sort_of_univ defs in
+	let kelim = allowed_sorts info s in
+	let ar = RegularArity 
+	  { mind_user_arity = ar; mind_sort = s; } in
+	  ar, kelim in
     (* Assigning VM tags to constructors *)
     let nconst, nblock = ref 0, ref 0 in
     let transf num =
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e57b0b4ad..9862ffd3e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -152,30 +152,93 @@ let sort_as_univ = function
 | Prop Null -> Universe.type0m
 | Prop Pos -> Universe.type0
 
+(* Template polymorphism *)
+
 let cons_subst u su subst =
   try
     (u, Universe.sup su (List.assoc_f Universe.eq u subst)) ::
       List.remove_assoc_f Universe.eq u subst
   with Not_found -> (u, su) :: subst
 
+let actualize_decl_level env lev t =
+  let sign,s = dest_arity env t in
+  mkArity (sign,lev)
+
+(* Bind expected levels of parameters to actual levels *)
+(* Propagate the new levels in the signature *)
+let rec make_subst env = function
+  | (_,Some _,_ as t)::sign, exp, args ->
+      let ctx,subst = make_subst env (sign, exp, args) in
+      t::ctx, subst
+  | d::sign, None::exp, args ->
+      let args = match args with _::args -> args | [] -> [] in
+      let ctx,subst = make_subst env (sign, exp, args) in
+      d::ctx, subst
+  | d::sign, Some u::exp, a::args ->
+      (* We recover the level of the argument, but we don't change the *)
+      (* level in the corresponding type in the arity; this level in the *)
+      (* arity is a global level which, at typing time, will be enforce *)
+      (* to be greater than the level of the argument; this is probably *)
+      (* a useless extra constraint *)
+      let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
+      let ctx,subst = make_subst env (sign, exp, args) in
+      d::ctx, cons_subst u s subst
+  | (na,None,t as d)::sign, Some u::exp, [] ->
+      (* No more argument here: we instantiate the type with a fresh level *)
+      (* which is first propagated to the corresponding premise in the arity *)
+      (* (actualize_decl_level), then to the conclusion of the arity (via *)
+      (* the substitution) *)
+      let ctx,subst = make_subst env (sign, exp, []) in
+	d::ctx, subst
+  | sign, [], _ ->
+      (* Uniform parameters are exhausted *)
+      sign,[]
+  | [], _, _ ->
+      assert false
+
 exception SingletonInductiveBecomesProp of Id.t
 
+let instantiate_universes env ctx ar argsorts =
+  let args = Array.to_list argsorts in
+  let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
+  let level = subst_large_constraints subst ar.template_level in
+  let ty =
+    (* Singleton type not containing types are interpretable in Prop *)
+    if is_type0m_univ level then prop_sort
+    (* Non singleton type not containing types are interpretable in Set *)
+    else if is_type0_univ level then set_sort
+    (* This is a Type with constraints *)
+    else Type level
+  in
+    (ctx, ty)
+
 (* Type of an inductive type *)
 
-let type_of_inductive_gen env ((mib,mip),u) =
-  let subst = make_inductive_subst mib u in
-    (subst_univs_constr subst mip.mind_arity.mind_user_arity, subst)
+let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
+  match mip.mind_arity with
+  | RegularArity a ->
+    let subst = make_inductive_subst mib u in
+      (subst_univs_constr subst a.mind_user_arity, subst)
+  | TemplateArity ar ->
+    let ctx = List.rev mip.mind_arity_ctxt in
+    let ctx,s = instantiate_universes env ctx ar paramtyps in
+      (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
+         the situation where a non-Prop singleton inductive becomes Prop
+         when applied to Prop params *)
+      if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s
+      then raise (SingletonInductiveBecomesProp mip.mind_typename);
+      mkArity (List.rev ctx,s), Univ.LMap.empty
 
 let type_of_inductive env pind = 
-  fst (type_of_inductive_gen env pind)
+  fst (type_of_inductive_gen env pind [||])
 
 let constrained_type_of_inductive env ((mib,mip),u as pind) =
-  let ty, subst = type_of_inductive_gen env pind in
+  let ty, subst = type_of_inductive_gen env pind [||] in
   let cst = instantiate_inductive_constraints mib subst in
     (ty, cst)
 
 let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = 
-  type_of_inductive env mip
+  fst (type_of_inductive_gen env mip args)
 
 (* The max of an array of universes *)
 
@@ -248,7 +311,9 @@ let local_rels ctxt =
 (* Get type of inductive, with parameters instantiated *)
 
 let inductive_sort_family mip =
-  family_of_sort mip.mind_arity.mind_sort
+  match mip.mind_arity with
+  | RegularArity s -> family_of_sort s.mind_sort
+  | TemplateArity _ -> InType
 
 let mind_arity mip =
   mip.mind_arity_ctxt, inductive_sort_family mip
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index c4a7452f0..a403003e2 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -109,6 +109,9 @@ exception SingletonInductiveBecomesProp of Id.t
 
 val max_inductive_sort : sorts array -> universe
 
+val instantiate_universes : env -> rel_context ->
+  template_arity -> constr Lazy.t array -> rel_context * sorts
+
 (** {6 Debug} *)
 
 type size = Large | Strict
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 2c093939a..56e94ba0d 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -277,8 +277,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let cb1 = Declareops.subst_const_body subst1 cb1 in
       let cb2 = Declareops.subst_const_body subst2 cb2 in
       (* Start by checking types*)
-      let typ1 = cb1.const_type in
-      let typ2 = cb2.const_type in
+      let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = check_type cst env typ1 typ2 in
       (* Now we check the bodies:
 	 - A transparent constant can only be implemented by a compatible
@@ -309,7 +309,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let arity1,cst1 = constrained_type_of_inductive env 
 	((mind1,mind1.mind_packets.(i)),u1) in
       let cst2 = UContext.constraints (Future.force cb2.const_universes) in
-      let typ2 = cb2.const_type in
+      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, arity1, typ2) in
        check_conv error cst infer_conv_leq env arity1 typ2
@@ -324,7 +324,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let u1 = inductive_instance mind1 in
       let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
       let cst2 = UContext.constraints (Future.force cb2.const_universes) in
-      let ty2 = cb2.const_type in
+      let ty2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, ty1, ty2) in
        check_conv error cst infer_conv env ty1 ty2
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a7f2125a7..c655e2f33 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -29,17 +29,20 @@ let prerr_endline =
   if debug then prerr_endline else fun _ -> ()
 
 let constrain_type env j poly = function
-  | `None -> j.uj_type
+  | `None -> 
+    if not poly then (* Old-style polymorphism *)
+      make_polymorphic_if_constant_for_ind env j
+    else RegularArity j.uj_type
   | `Some t ->
       let tj = infer_type env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
-	t
+	RegularArity t
   | `SomeWJ (t, tj) ->
       let tj = infer_type env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
-	t
+	RegularArity t
 
 let map_option_typ = function None -> `None | Some x -> `Some x
 
@@ -72,12 +75,12 @@ let handle_side_effects env body side_eff =
       | Undef _ -> assert false
       | Def b ->
           let b = Mod_subst.force_constr b in
-          let b_ty = cb.const_type in
+          let b_ty = Typeops.type_of_constant_type env cb.const_type in
           let t = sub c 1 (Vars.lift 1 t) in
           mkLetIn (cname c, b, b_ty, t)
       | OpaqueDef b -> 
           let b = Opaqueproof.force_proof b in
-          let b_ty = cb.const_type in
+          let b_ty = Typeops.type_of_constant_type env cb.const_type in
           let t = sub c 1 (Vars.lift 1 t) in
           mkApp (mkLambda (cname c, b_ty, t), [|b|]) in
     List.fold_right fix_body cbl t
@@ -98,7 +101,7 @@ let infer_declaration env kn dcl =
       let env = push_context uctx env in
       let j = infer env t in
       let t = hcons_constr (Typeops.assumption_of_judgment env j) in
-      Undef nl, t, None, poly, Future.from_val uctx, false, ctx
+      Undef nl, RegularArity t, None, poly, Future.from_val uctx, false, ctx
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true } as c) ->
       let env = push_context (Future.join c.const_entry_universes) env in (* FIXME *)
@@ -113,7 +116,7 @@ let infer_declaration env kn dcl =
           feedback_completion_typecheck feedback_id;
           j.uj_val, Univ.empty_constraint) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
-      def, typ, None, c.const_entry_polymorphic, c.const_entry_universes,
+      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 (Future.join c.const_entry_universes) env in (* FIXME *)
@@ -129,13 +132,13 @@ let infer_declaration env kn dcl =
       def, typ, None, c.const_entry_polymorphic,
         c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx
 
-(* let global_vars_set_constant_type env = function *)
-(*   | NonPolymorphicType t -> global_vars_set env t *)
-(*   | PolymorphicArity (ctx,_) -> *)
-(*       Context.fold_rel_context *)
-(*         (fold_rel_declaration *)
-(* 	  (fun t c -> Id.Set.union (global_vars_set env t) c)) *)
-(*       ctx ~init:Id.Set.empty *)
+let global_vars_set_constant_type env = function
+  | RegularArity t -> global_vars_set env t
+  | TemplateArity (ctx,_) ->
+      Context.fold_rel_context
+        (fold_rel_declaration
+	  (fun t c -> Id.Set.union (global_vars_set env t) c))
+      ctx ~init:Id.Set.empty
 
 let record_aux env s1 s2 =
   let v =
@@ -162,7 +165,7 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
     | None when not (List.is_empty context_ids) -> 
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
-        let ids_typ = global_vars_set env typ in
+        let ids_typ = global_vars_set_constant_type env typ in
         let ids_def = match def with
         | Undef _ -> Idset.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
@@ -186,14 +189,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         match def with
         | Undef _ as x -> x (* nothing to check *)
         | Def cs as x ->
-            let ids_typ = global_vars_set env typ in
+            let ids_typ = global_vars_set_constant_type env typ in
             let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
             let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
             OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
-              let ids_typ = global_vars_set env typ in
+              let ids_typ = global_vars_set_constant_type env typ in
               let ids_def = global_vars_set env c in
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
               check declared inferred) lc) in
@@ -229,6 +232,7 @@ let translate_recipe env kn r =
 let translate_local_def env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
     infer_declaration env None (DefinitionEntry centry) in
+  let typ = type_of_constant_type env typ in
   def, typ, univs
 
 (* Insertion of inductive types. *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 09fd4cc7f..09e2fb1d5 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -113,20 +113,62 @@ let check_hyps_inclusion env c sign =
 
 (* Make a type polymorphic if an arity *)
 
+let extract_level env p =
+  let _,c = dest_prod_assum env p in
+  match kind_of_term c with Sort (Type u) -> Some u | _ -> None
+
+let extract_context_levels env l =
+  let fold l (_, b, p) = match b with
+  | None -> extract_level env p :: l
+  | _ -> l
+  in
+  List.fold_left fold [] l
+
+let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
+  let params, ccl = dest_prod_assum env t in
+  match kind_of_term ccl with
+  | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) ->
+      let param_ccls = extract_context_levels env params in
+      let s = { template_param_levels = param_ccls; template_level = u} in
+      TemplateArity (params,s)
+  | _ ->
+      RegularArity t
+
 (* Type of constants *)
 
-let type_of_constant env cst = constant_type env cst
-let type_of_constant_in env cst = constant_type_in env cst
-let type_of_constant_knowing_parameters env t _ = t
-let type_of_constant_type env cst = cst
+let type_of_constant_type_knowing_parameters env t paramtyps =
+  match t with
+  | RegularArity t -> t
+  | TemplateArity (sign,ar) ->
+      let ctx = List.rev sign in
+      let ctx,s = instantiate_universes env ctx ar paramtyps in
+      mkArity (List.rev ctx,s)
+
+let type_of_constant_knowing_parameters env cst paramtyps =
+  let ty, cu = constant_type env cst in
+    type_of_constant_type_knowing_parameters env ty paramtyps, cu
+
+let type_of_constant_type env t =
+  type_of_constant_type_knowing_parameters env t [||]
 
-let judge_of_constant env (kn,u as cst) =
+let type_of_constant env cst =
+  type_of_constant_knowing_parameters env cst [||]
+
+let type_of_constant_in env cst =
+  let ar = constant_type_in env cst in
+    type_of_constant_type_knowing_parameters env ar [||]
+
+let judge_of_constant_knowing_parameters env (kn,u as cst) jl =
   let c = mkConstU cst in
   let cb = lookup_constant kn env in
   let _ = check_hyps_inclusion env c cb.const_hyps in
-  let ty, cu = type_of_constant env cst in
+  let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
+  let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
   let _ = Environ.check_constraints cu env in
-    (make_judge c ty)
+    make_judge c ty
+
+let judge_of_constant env cst =
+  judge_of_constant_knowing_parameters env cst [||]
 
 let type_of_projection env (cst,u) =
   let cb = lookup_constant cst env in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 6bc1ce496..9747dbe83 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -51,10 +51,13 @@ val judge_of_relative : env -> int -> unsafe_judgment
 val judge_of_variable : env -> variable -> unsafe_judgment
 
 (** {6 type of a constant } *)
-val judge_of_constant : env -> constant puniverses -> unsafe_judgment
 
-(* val judge_of_constant_knowing_parameters : *)
-(*   env -> constant -> unsafe_judgment array -> unsafe_judgment *)
+val judge_of_constant : env -> pconstant -> unsafe_judgment
+
+val judge_of_constant_knowing_parameters :
+  env -> pconstant -> unsafe_judgment array -> unsafe_judgment
+
+(** {6 type of an applied projection } *)
 
 val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment
 
@@ -103,15 +106,20 @@ val judge_of_case : env -> case_info
 val type_fixpoint : env -> Name.t array -> types array
     -> unsafe_judgment array -> unit
 
-val type_of_constant : env -> constant puniverses -> types constrained
+val type_of_constant : env -> pconstant -> types constrained
 
 val type_of_constant_type : env -> constant_type -> types
 
 val type_of_projection : env -> Names.projection puniverses -> types
 
-val type_of_constant_in : env -> constant puniverses -> types
+val type_of_constant_in : env -> pconstant -> types
 
-val type_of_constant_knowing_parameters :
+val type_of_constant_type_knowing_parameters :
   env -> constant_type -> types Lazy.t array -> types
 
+val type_of_constant_knowing_parameters :
+  env -> pconstant -> types Lazy.t array -> types constrained
 
+(** Make a type polymorphic if an arity *)
+val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
+  constant_type