Merge PR #8303: Better controls for template polymorphism

11 files changed, 190 insertions, 70 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 3d3a1b11b1..35f45e2e0e 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1025,8 +1025,26 @@ the Type hierarchy.
 Template polymorphism
 +++++++++++++++++++++
 
-Inductive types declared in :math:`\Type` are polymorphic over their arguments
-in :math:`\Type`. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}`
+Inductive types can be made polymorphic over their arguments
+in :math:`\Type`.
+
+.. opt:: Auto Template Polymorphism
+
+  This option, enabled by default, makes every inductive type declared
+  at level :math:`Type` (without annotations or hiding it behind a
+  definition) template polymorphic.
+
+  This can be prevented using the ``notemplate`` attribute.
+
+  An inductive type can be forced to be template polymorphic using the
+  ``template`` attribute.
+
+  Template polymorphism and universe polymorphism (see Chapter
+  :ref:`polymorphicuniverses`) are incompatible, so if the later is
+  enabled it will prevail over automatic template polymorphism and
+  cause an error when using the ``template`` attribute.
+
+If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}`
 for the arity obtained from :math:`A` by replacing its sort with :math:`s`.
 Especially, if :math:`A` is well-typed in some global environment and local
 context, then :math:`A_{/s}` is typable by typability of all products in the
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index d7eb865e0a..f79e5270a2 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -280,7 +280,7 @@ let typecheck_inductive env mie =
     List.fold_left
       (fun (env_ar,l) ind ->
          (* Arities (without params) are typed-checked here *)
-	 let expltype = ind.mind_entry_template in
+         let template = ind.mind_entry_template in
          let arity =
 	   if isArity ind.mind_entry_arity then
 	     let (ctx,s) = dest_arity env_params ind.mind_entry_arity in
@@ -316,7 +316,7 @@ let typecheck_inductive env mie =
 	 let env_ar' =
            push_rel (LocalAssum (Name id, full_arity)) env_ar in
              (* (add_constraints cst2 env_ar) in *)
-	   (env_ar', (id,full_arity,sign @ paramsctxt,expltype,deflev,inflev)::l))
+           (env_ar', (id,full_arity,sign @ paramsctxt,template,deflev,inflev)::l))
       (env',[])
       mie.mind_entry_inds in
 
@@ -343,7 +343,7 @@ let typecheck_inductive env mie =
   (* Compute/check the sorts of the inductive types *)
 
   let inds =
-    Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,clev)  ->
+    Array.map (fun ((id,full_arity,sign,template,def_level,inf_level),cn,lc,clev)  ->
       let infu = 
 	(** Inferred level, with parameters and constructors. *)
 	match inf_level with
@@ -369,31 +369,34 @@ let typecheck_inductive env mie =
 	  RegularArity (not is_natural,full_arity,defu)
       in
       let template_polymorphic () =
-	let sign, s =
+        let _, s =
           try dest_arity env full_arity
           with NotArity -> raise (InductiveError (NotAnArity (env, full_arity)))
-	in
-	  match s with
-	  | Type u when expltype (* Explicitly polymorphic *) ->
-	    (* The polymorphic level is a function of the level of the *)
-	    (* conclusions of the parameters *)
-            (* We enforce [u >= lev] in case [lev] has a strict upper *)
-            (* constraints over [u] *)
-	    let b = type_in_type env || UGraph.check_leq (universes env') infu u in
-	      if not b then
-		anomaly ~label:"check_inductive" 
-		  (Pp.str"Incorrect universe " ++
-		     Universe.pr u ++ Pp.str " declared for inductive type, inferred level is "
-		   ++ Universe.pr clev ++ Pp.str ".")
-	      else
-		TemplateArity (param_ccls paramsctxt, infu)
-	  | _ (* Not an explicit occurrence of Type *) ->
-	    full_polymorphic ()
+        in
+        let u = Sorts.univ_of_sort s in
+        (* The polymorphic level is a function of the level of the *)
+        (* conclusions of the parameters *)
+        (* We enforce [u >= lev] in case [lev] has a strict upper *)
+        (* constraints over [u] *)
+        let b = type_in_type env || UGraph.check_leq (universes env') infu u in
+        if not b then
+          anomaly ~label:"check_inductive"
+            (Pp.str"Incorrect universe " ++
+             Universe.pr u ++ Pp.str " declared for inductive type, inferred level is "
+             ++ Universe.pr clev ++ Pp.str ".")
+        else
+          TemplateArity (param_ccls paramsctxt, infu)
       in
       let arity =
         match mie.mind_entry_universes with
-        | Monomorphic_ind_entry _ -> template_polymorphic ()
-        | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> full_polymorphic ()
+        | Monomorphic_ind_entry _ ->
+          if template then template_polymorphic ()
+          else full_polymorphic ()
+        | Polymorphic_ind_entry _ | Cumulative_ind_entry _ ->
+          if template
+          then anomaly ~label:"polymorphic_template_ind"
+              Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.")
+          else full_polymorphic ()
       in
 	(id,cn,lc,(sign,arity)))
     inds
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 5fc4293cbb..bbc0a37c69 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1499,7 +1499,7 @@ let do_build_inductive
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
+      (Flags.silently (ComInductive.do_mutual_inductive ~template:None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
       Declarations.Finite
   with
     | UserError(s,msg) as e ->
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
new file mode 100644
index 0000000000..1c6e2d81d8
--- /dev/null
+++ b/test-suite/success/Template.v
@@ -0,0 +1,48 @@
+Set Printing Universes.
+
+Module AutoYes.
+  Inductive Box (A:Type) : Type := box : A -> Box A.
+
+  About Box.
+
+  (* This checks that Box is template poly, see module No for how it fails *)
+  Universe i j. Constraint i < j.
+  Definition j_lebox (A:Type@{j}) := Box A.
+  Definition box_lti A := Box A : Type@{i}.
+
+End AutoYes.
+
+Module AutoNo.
+  Unset Auto Template Polymorphism.
+  Inductive Box (A:Type) : Type := box : A -> Box A.
+
+  About Box.
+
+  Universe i j. Constraint i < j.
+  Definition j_lebox (A:Type@{j}) := Box A.
+  Fail Definition box_lti A := Box A : Type@{i}.
+
+End AutoNo.
+
+Module Yes.
+  #[template]
+  Inductive Box@{i} (A:Type@{i}) : Type@{i} := box : A -> Box A.
+
+  About Box.
+
+  Universe i j. Constraint i < j.
+  Definition j_lebox (A:Type@{j}) := Box A.
+  Definition box_lti A := Box A : Type@{i}.
+
+End Yes.
+
+Module No.
+  #[notemplate]
+  Inductive Box (A:Type) : Type := box : A -> Box A.
+
+  About Box.
+
+  Universe i j. Constraint i < j.
+  Definition j_lebox (A:Type@{j}) := Box A.
+  Fail Definition box_lti A := Box A : Type@{i}.
+End No.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 716c40dbff..fb9d21c429 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -35,6 +35,18 @@ module RelDecl = Context.Rel.Declaration
 
 (* 3b| Mutual inductive definitions *)
 
+let should_auto_template =
+  let open Goptions in
+  let auto = ref true in
+  let _ = declare_bool_option
+      { optdepr  = false;
+        optname  = "Automatically make some inductive types template polymorphic";
+        optkey   = ["Auto";"Template";"Polymorphism"];
+        optread  = (fun () -> !auto);
+        optwrite = (fun b -> auto := b); }
+  in
+  fun () -> !auto
+
 let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
   | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
   | CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c)
@@ -113,17 +125,16 @@ let rec check_anonymous_type ind =
     | GCast (e, _) -> check_anonymous_type e
     | _ -> false
 
-let make_conclusion_flexible sigma ty poly =
-  if poly && Term.isArity ty then
-    let _, concl = Term.destArity ty in
-      match concl with
-      | Type u ->
-        (match Univ.universe_level u with
+let make_conclusion_flexible sigma = function
+  | None -> sigma
+  | Some s ->
+    (match EConstr.ESorts.kind sigma s with
+     | Type u ->
+       (match Univ.universe_level u with
         | Some u ->
           Evd.make_flexible_variable sigma ~algebraic:true u
         | None -> sigma)
-      | _ -> sigma
-  else sigma
+     | _ -> sigma)
 
 let is_impredicative env u =
   u = Prop || (is_impredicative_set env && u = Set)
@@ -133,10 +144,12 @@ let interp_ind_arity env sigma ind =
   let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
   let sigma,t = understand_tcc env sigma ~expected_type:IsType c in
   let pseudo_poly = check_anonymous_type c in
-  let () = if not (Reductionops.is_arity env sigma t) then
+  match Reductionops.sort_of_arity env sigma t with
+  | exception Invalid_argument _ ->
     user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
-  in
-  sigma, (t, pseudo_poly, impls)
+  | s ->
+    let concl = if pseudo_poly then Some s else None in
+    sigma, (t, concl, impls)
 
 let interp_cstrs env sigma impls mldata arity ind =
   let cnames,ctyps = List.split ind.ind_lc in
@@ -335,7 +348,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
   let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
   Evd.restrict_universe_context sigma uvars
 
-let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly prv finite =
+let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations cum poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
   if not (List.is_empty uparamsl) && not (List.is_empty notations)
@@ -363,7 +376,7 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun (_, _, impls) -> userimpls @
     lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
-  let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
+  let arities = List.map pi1 arities and arityconcl = List.map pi2 arities in
   let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
   let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
@@ -402,13 +415,14 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
   let nf = Evarutil.nf_evars_universes sigma in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let arities = List.map EConstr.(to_constr sigma) arities in
-  let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in
+  let sigma = List.fold_left make_conclusion_flexible sigma arityconcl in
   let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
   let sigma = Evd.minimize_universes sigma in
   let nf = Evarutil.nf_evars_universes sigma in
   let arities = List.map nf arities in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
+  let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in
   let sigma = restrict_inductive_universes sigma ctx_params arities constructors in
   let uctx = Evd.check_univ_decl ~poly sigma decl in
   List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities;
@@ -418,13 +432,23 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
     constructors;
 
   (* Build the inductive entries *)
-  let entries = List.map4 (fun ind arity template (cnames,ctypes,cimpls) -> {
-    mind_entry_typename = ind.ind_name;
-    mind_entry_arity = arity;
-    mind_entry_template = template;
-    mind_entry_consnames = cnames;
-    mind_entry_lc = ctypes
-  }) indl arities aritypoly constructors in
+  let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) ->
+      let template = match template with
+        | Some template ->
+          if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+          template
+        | None ->
+          should_auto_template () && not poly &&
+          Option.cata (fun s -> not (Sorts.is_small s)) false concl
+      in
+      { mind_entry_typename = ind.ind_name;
+        mind_entry_arity = arity;
+        mind_entry_template = template;
+        mind_entry_consnames = cnames;
+        mind_entry_lc = ctypes
+      })
+      indl arities arityconcl constructors
+  in
   let impls =
     let len = Context.Rel.nhyps ctx_params in
       List.map2 (fun indimpls (_,_,cimpls) ->
@@ -454,8 +478,8 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
       InferCumulativity.infer_inductive env_ar mind_ent
    else mind_ent), Evd.universe_binders sigma, impls
 
-let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
-  interp_mutual_inductive_gen (Global.env()) ([],paramsl,indl) notations cum poly prv finite
+let interp_mutual_inductive ~template (paramsl,indl) notations cum poly prv finite =
+  interp_mutual_inductive_gen (Global.env()) ~template ([],paramsl,indl) notations cum poly prv finite
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
@@ -543,11 +567,11 @@ type uniform_inductive_flag =
   | UniformParameters
   | NonUniformParameters
 
-let do_mutual_inductive indl cum poly prv ~uniform finite =
+let do_mutual_inductive ~template indl cum poly prv ~uniform finite =
   let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
   let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
-  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) indl ntns cum poly prv finite in
+  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template indl ntns cum poly prv finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (declare_mutual_inductive_with_eliminations mie pl impls);
   (* Declare the possible notations of inductive types *)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 4e30ed7de5..8a2c9b8719 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -24,7 +24,7 @@ type uniform_inductive_flag =
   | NonUniformParameters
 
 val do_mutual_inductive :
-  (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
+  template:bool option -> (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
   polymorphic -> private_flag -> uniform:uniform_inductive_flag ->
   Declarations.recursivity_kind -> unit
 
@@ -45,6 +45,8 @@ val declare_mutual_inductive_with_eliminations :
   mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
   MutInd.t
 
+val should_auto_template : unit -> bool
+
 (** Exported for Funind *)
 
 (** Extracting the semantical components out of the raw syntax of mutual
@@ -67,6 +69,6 @@ val extract_mutual_inductive_declaration_components :
 (** Typing mutual inductive definitions *)
 
 val interp_mutual_inductive :
-  structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
+  template:bool option -> structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
   polymorphic -> private_flag -> Declarations.recursivity_kind ->
   mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
diff --git a/vernac/record.ml b/vernac/record.ml
index 6b5c538df2..d36586d062 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -393,14 +393,14 @@ open Typeclasses
 
 let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
   let nparams = List.length params in
-  let template, ctx =
+  let poly, ctx =
     match univs with
     | Monomorphic_ind_entry ctx ->
-      template, Monomorphic_const_entry Univ.ContextSet.empty
+      false, Monomorphic_const_entry Univ.ContextSet.empty
     | Polymorphic_ind_entry ctx ->
-      false, Polymorphic_const_entry ctx
+      true, Polymorphic_const_entry ctx
     | Cumulative_ind_entry cumi ->
-      false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
+      true, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
   in
   let binder_name =
     match name with
@@ -417,6 +417,18 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
     let args = Context.Rel.to_extended_list mkRel nfields params in
     let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
     let type_constructor = it_mkProd_or_LetIn ind fields in
+    let template =
+      match template with
+      | Some template, _ ->
+        (* templateness explicitly requested *)
+        if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+        template
+      | None, template ->
+        (* auto detect template *)
+        ComInductive.should_auto_template () && template && not poly &&
+        let _, s = Reduction.dest_arity (Global.env()) arity in
+        not (Sorts.is_small s)
+    in
     { mind_entry_typename = id;
       mind_entry_arity = arity;
       mind_entry_template = template;
@@ -441,7 +453,6 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
     let cstr = (rsp, 1) in
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in
     let build = ConstructRef cstr in
-    let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in
     let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
     let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in
     rsp
@@ -656,13 +667,14 @@ let extract_record_data records =
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions
    or subinstances. *)
-let definition_structure kind cum poly finite records =
+let definition_structure kind ~template cum poly finite records =
   let () = check_unique_names records in
   let () = check_priorities kind records in
   let pl, ps, data = extract_record_data records in
-  let pl, univs, template, params, implpars, data =
+  let pl, univs, auto_template, params, implpars, data =
     States.with_state_protection (fun () ->
-      typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in
+        typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in
+  let template = template, auto_template in
   match kind with
   | Class def ->
     let (_, id, _, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
diff --git a/vernac/record.mli b/vernac/record.mli
index 567f2b3138..055a17895a 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,7 +26,8 @@ val declare_projections :
     (Name.t * bool) list * Constant.t option list
 
 val definition_structure :
-  inductive_kind -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
+  inductive_kind -> template:bool option ->
+  Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
   Declarations.recursivity_kind ->
   (coercion_flag *
   Names.lident *
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 681dce3ca3..e6b3721134 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -555,7 +555,7 @@ let should_treat_as_uniform () =
   then ComInductive.UniformParameters
   else ComInductive.NonUniformParameters
 
-let vernac_record cum k poly finite records =
+let vernac_record ~template cum k poly finite records =
   let is_cumulative = should_treat_as_cumulative cum poly in
   let map ((coe, (id, pl)), binders, sort, nameopt, cfs) =
     let const = match nameopt with
@@ -577,7 +577,7 @@ let vernac_record cum k poly finite records =
     coe, id, pl, binders, cfs, const, sort
   in
   let records = List.map map records in
-  ignore(Record.definition_structure k is_cumulative poly finite records)
+  ignore(Record.definition_structure ~template k is_cumulative poly finite records)
 
 (** When [poly] is true the type is declared polymorphic. When [lo] is true,
     then the type is declared private (as per the [Private] keyword). [finite]
@@ -606,13 +606,14 @@ let vernac_inductive ~atts cum lo finite indl =
   | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l)
   | _ -> None
   in
+  let template = atts.template in
   if Option.has_some is_defclass then
     (** Definitional class case *)
     let (id, bl, c, l) = Option.get is_defclass in
     let (coe, (lid, ce)) = l in
     let coe' = if coe then Some true else None in
     let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
-    vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
+    vernac_record ~template cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (** Mutual record case *)
     let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -635,7 +636,7 @@ let vernac_inductive ~atts cum lo finite indl =
     let ((_, _, _, kind, _), _) = List.hd indl in
     let kind = match kind with Class _ -> Class false | _ -> kind in
     let recordl = List.map unpack indl in
-    vernac_record cum kind atts.polymorphic finite recordl
+    vernac_record ~template cum kind atts.polymorphic finite recordl
   else if List.for_all is_constructor indl then
     (** Mutual inductive case *)
     let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -661,7 +662,7 @@ let vernac_inductive ~atts cum lo finite indl =
     let indl = List.map unpack indl in
     let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
     let uniform = should_treat_as_uniform () in
-    ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo ~uniform finite
+    ComInductive.do_mutual_inductive ~template indl is_cumulative atts.polymorphic lo ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")
 (*
@@ -2358,6 +2359,14 @@ let attributes_of_flags f atts =
          (Some false, atts)
        | ("polymorphic" | "monomorphic") ->
          user_err Pp.(str "Polymorphism specified twice")
+       | "template" when atts.template = None ->
+         assert_empty k v;
+         polymorphism, { atts with template = Some true }
+       | "notemplate" when atts.template = None ->
+         assert_empty k v;
+         polymorphism, { atts with template = Some false }
+       | "template" | "notemplate" ->
+         user_err Pp.(str "Templateness specified twice")
        | "local" when Option.is_empty atts.locality ->
          assert_empty k v;
          (polymorphism, { atts with locality = Some true })
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1bb1414f3d..2746cbd144 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -21,12 +21,13 @@ type atts = {
   loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
+  template : bool option;
   program : bool;
   deprecated : deprecation option;
 }
 
-let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts =
-  { loc ; locality ; polymorphic ; program ; deprecated }
+let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () : atts =
+  { loc ; locality ; polymorphic ; program ; deprecated; template }
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 46468b3098..62a178b555 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -18,12 +18,14 @@ type atts = {
   loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
+  template : bool option;
   program : bool;
   deprecated : deprecation option;
 }
 
 val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
-  ?polymorphic: bool -> ?program: bool -> ?deprecated: deprecation option -> unit -> atts
+  ?polymorphic: bool -> ?template:bool option ->
+  ?program: bool -> ?deprecated: deprecation option -> unit -> atts
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t