Remove the Template Check option.

23 files changed, 21 insertions, 140 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 051f51bbb3..62e732ce69 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -170,7 +170,6 @@ let check_inductive env mind mb =
          check_guarded = mb_flags.check_guarded;
          check_positive = mb_flags.check_positive;
          check_universes = mb_flags.check_universes;
-         check_template = mb_flags.check_template;
          conv_oracle = mb_flags.conv_oracle;
         }
         env
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index d115744707..8854a23dd5 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -56,10 +56,6 @@ let pr_nonpositive env =
   let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in
   pr_assumptions "Inductives whose positivity is assumed" inds
 
-let pr_unsafe_template env =
-  let inds = fold_inductives  (fun c cb acc -> if not cb.mind_typing_flags.check_template then MutInd.to_string c :: acc else acc) env [] in
-  pr_assumptions "Inductives using unchecked template polymorphism" inds
-
 let print_context env =
   if !output_context then begin
     Feedback.msg_notice
@@ -70,8 +66,8 @@ let print_context env =
       str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++
-      str "* " ++ hov 0 (pr_nonpositive env ++ fnl()) ++ fnl() ++
-      str "* " ++ hov 0 (pr_unsafe_template env)))
+      str "* " ++ hov 0 (pr_nonpositive env ++ fnl()))
+      )
   end
 
 let stats env =
diff --git a/checker/values.ml b/checker/values.ml
index c8bbc092b4..ed730cff8e 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -238,7 +238,7 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool; v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
 
 let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f1eb000c88..31dd26d2ba 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -258,17 +258,6 @@ let cook_constant { from = cb; info } =
 (********************************)
 (* Discharging mutual inductive *)
 
-let template_level_of_var ~template_check d =
-  (* When [template_check], a universe from a section variable may not
-     be in the universes from the inductive (it must be pre-declared)
-     so always [None]. *)
-  if template_check then None
-  else
-    let c = Term.strip_prod_assum (RelDecl.get_type d) in
-    match kind c with
-    | Sort (Type u) -> Univ.Universe.level u
-    | _ -> None
-
 let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c)
 
 let abstract_rel_ctx (section_decls,subst) ctx =
@@ -305,7 +294,7 @@ let abstract_projection ~params expmod hyps t =
   let _, t = decompose_prod_n_assum (List.length params + 1 + Context.Rel.nhyps (fst hyps)) t in
   t
 
-let cook_one_ind ~template_check ~ntypes
+let cook_one_ind ~ntypes
     (section_decls,_ as hyps) expmod mip =
   let mind_arity = match mip.mind_arity with
     | RegularArity {mind_user_arity=arity;mind_sort=sort} ->
@@ -314,7 +303,7 @@ let cook_one_ind ~template_check ~ntypes
       RegularArity {mind_user_arity=arity; mind_sort=sort}
     | TemplateArity {template_param_levels=levels;template_level;template_context} ->
       let sec_levels = CList.map_filter (fun d ->
-          if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d)
+          if RelDecl.is_local_assum d then Some None
           else None)
           section_decls
       in
@@ -362,14 +351,13 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
   let removed_vars = Context.Named.to_vars section_decls in
   let section_decls, _ as hyps = abstract_context section_decls in
   let nnewparams = Context.Rel.nhyps section_decls in
-  let template_check = mib.mind_typing_flags.check_template in
   let mind_params_ctxt =
     let ctx = Context.Rel.map expmod mib.mind_params_ctxt in
     abstract_rel_ctx hyps ctx
   in
   let ntypes = mib.mind_ntypes in
   let mind_packets =
-    Array.map (cook_one_ind ~template_check ~ntypes hyps expmod)
+    Array.map (cook_one_ind ~ntypes hyps expmod)
       mib.mind_packets
   in
   let mind_record = match mib.mind_record with
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index c550b0d432..ac130d018d 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -89,10 +89,6 @@ type typing_flags = {
   indices_matter: bool;
   (** The universe of an inductive type must be above that of its indices. *)
 
-  check_template : bool;
-  (* If [false] then we don't check that the universes template-polymorphic
-     inductive parameterize on are necessarily local and unbounded from below.
-     This potentially introduces inconsistencies. *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 047027984d..a3adac7a11 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,7 +26,6 @@ let safe_flags oracle = {
   enable_VM = true;
   enable_native_compiler = true;
   indices_matter = true;
-  check_template = true;
 }
 
 (** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index f04863386f..87f2f234da 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -275,7 +275,6 @@ let type_in_type env = not (typing_flags env).check_universes
 let deactivated_guard env = not (typing_flags env).check_guarded
 
 let indices_matter env = env.env_typing_flags.indices_matter
-let check_template env = env.env_typing_flags.check_template
 
 let universes env = env.env_stratification.env_universes
 let universes_lbound env = env.env_stratification.env_universes_lbound
@@ -449,7 +448,6 @@ let same_flags {
      share_reduction;
      enable_VM;
      enable_native_compiler;
-     check_template;
   } alt =
   check_guarded == alt.check_guarded &&
   check_positive == alt.check_positive &&
@@ -458,8 +456,7 @@ let same_flags {
   indices_matter == alt.indices_matter &&
   share_reduction == alt.share_reduction &&
   enable_VM == alt.enable_VM &&
-  enable_native_compiler == alt.enable_native_compiler &&
-  check_template == alt.check_template
+  enable_native_compiler == alt.enable_native_compiler
 [@warning "+9"]
 
 let set_typing_flags c env = (* Unsafe *)
@@ -591,9 +588,6 @@ let polymorphic_pind (ind,u) env =
 let type_in_type_ind (mind,_i) env =
   not (lookup_mind mind env).mind_typing_flags.check_universes
 
-let template_checked_ind (mind,_i) env =
-  (lookup_mind mind env).mind_typing_flags.check_template
-
 let template_polymorphic_ind (mind,i) env =
   match (lookup_mind mind env).mind_packets.(i).mind_arity with
   | TemplateArity _ -> true
@@ -802,14 +796,6 @@ let get_template_polymorphic_variables env r =
   | IndRef ind -> template_polymorphic_variables ind env
   | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env
 
-let is_template_checked env r =
-  let open Names.GlobRef in
-  match r with
-  | VarRef _id -> false
-  | ConstRef _c -> false
-  | IndRef ind -> template_checked_ind ind env
-  | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env
-
 let is_type_in_type env r =
   let open Names.GlobRef in
   match r with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index bd5a000c2b..e80d0a9b9f 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -112,7 +112,6 @@ val is_impredicative_set : env -> bool
 val type_in_type : env -> bool
 val deactivated_guard : env -> bool
 val indices_matter : env -> bool
-val check_template : env -> bool
 
 val is_impredicative_sort : env -> Sorts.t -> bool
 val is_impredicative_univ : env -> Univ.Universe.t -> bool
@@ -274,7 +273,6 @@ val type_in_type_ind : inductive -> env -> bool
 val template_polymorphic_ind : inductive -> env -> bool
 val template_polymorphic_variables : inductive -> env -> Univ.Level.t list
 val template_polymorphic_pind : pinductive -> env -> bool
-val template_checked_ind : inductive -> env -> bool
 
 (** {5 Modules } *)
 
@@ -373,7 +371,6 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat
 val is_polymorphic : env -> Names.GlobRef.t -> bool
 val is_template_polymorphic : env -> GlobRef.t -> bool
 val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list
-val is_template_checked : env -> GlobRef.t -> bool
 val is_type_in_type : env -> GlobRef.t -> bool
 
 (** Native compiler *)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 113ee787f2..cc15109f06 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -197,7 +197,7 @@ let unbounded_from_below u cstrs =
    (starting from the most recent and ignoring let-definitions) is not
    contributing to the inductive type's sort or is Some u_k if its level
    is u_k and is contributing. *)
-let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl =
+let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl =
   let check_level l =
     Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
     unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
@@ -205,27 +205,23 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc
   in
   let univs = Univ.Universe.levels concl in
   let univs =
-    if template_check then
-      Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
-    else univs (* Doesn't check the universes can be generalized *)
+    Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
   in
   let fold acc = function
     | (LocalAssum (_, p)) ->
       (let c = Term.strip_prod_assum p in
       match kind c with
         | Sort (Type u) ->
-          if template_check then
             (match Univ.Universe.level u with
              | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None
              | None -> None)
-          else Univ.Universe.level u
         | _ -> None) :: acc
     | LocalDef _ -> acc
   in
   let params = List.fold_left fold [] paramsctxt in
   params, univs
 
-let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
   if not (Universe.Set.is_empty univ_info.missing)
   then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ)));
   let arity = Vars.subst_univs_level_constr usubst arity in
@@ -267,9 +263,9 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
           splayed_lc
       in
       let param_levels, concl_levels =
-        template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ
+        template_polymorphic_univs ~ctor_levels ctx params min_univ
       in
-      if template_check && List.for_all (fun x -> Option.is_empty x) param_levels
+      if List.for_all (fun x -> Option.is_empty x) param_levels
          && Univ.LSet.is_empty concl_levels then
         CErrors.user_err
           Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
@@ -356,8 +352,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
   (* Abstract universes *)
   let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
   let params = Vars.subst_univs_level_context usubst params in
-  let template_check = Environ.check_template env in
-  let data = List.map (abstract_packets ~template_check univs usubst params) data in
+  let data = List.map (abstract_packets univs usubst params) data in
 
   let env_ar_par =
     let ctx = Environ.rel_context env_ar_par in
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 8dea8f046d..723ba5459e 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -40,7 +40,6 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
 (* Utility function to compute the actual universe parameters
    of a template polymorphic inductive *)
 val template_polymorphic_univs :
-  template_check:bool ->
   ctor_levels:Univ.LSet.t ->
   Univ.ContextSet.t ->
   Constr.rel_context ->
diff --git a/library/global.ml b/library/global.ml
index fbbe09301b..8706238f5a 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -192,8 +192,6 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r
 
 let is_template_polymorphic r = is_template_polymorphic (env ()) r
 
-let is_template_checked r = is_template_checked (env ()) r
-
 let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r
 
 let is_type_in_type r = is_type_in_type (env ()) r
diff --git a/library/global.mli b/library/global.mli
index b6bd69c17c..0198ac5952 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -150,7 +150,6 @@ val is_joined_environment : unit -> bool
 
 val is_polymorphic : GlobRef.t -> bool
 val is_template_polymorphic : GlobRef.t -> bool
-val is_template_checked : GlobRef.t -> bool
 val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list
 val is_type_in_type : GlobRef.t -> bool
 
diff --git a/printing/printer.ml b/printing/printer.ml
index 97e0528939..8af4d1d932 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -859,8 +859,6 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
-  | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism
-                                       on parameter universes has not been checked. *)
   | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =
@@ -880,13 +878,10 @@ struct
         Constant.CanOrd.compare k1 k2
     | Positive m1 , Positive m2 ->
         MutInd.CanOrd.compare m1 m2
-    | TemplatePolymorphic m1, TemplatePolymorphic m2 ->
-        MutInd.CanOrd.compare m1 m2
     | Guarded k1 , Guarded k2 ->
         GlobRef.Ordered.compare k1 k2
     | _ , Constant _ -> 1
     | _ , Positive _ -> 1
-    | _, TemplatePolymorphic _ -> 1
     | _ -> -1
 
   let compare x y =
@@ -947,9 +942,6 @@ let pr_assumptionset env sigma s =
           hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.")
       | Guarded gr ->
           hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.")
-      | TemplatePolymorphic m ->
-          hov 2 (safe_pr_inductive env m ++ spc () ++
-                 strbrk"is assumed template polymorphic on all its universe parameters.")
       | TypeInType gr ->
          hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
     in
diff --git a/printing/printer.mli b/printing/printer.mli
index 1d7a25cbb6..cd5151bd8f 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -231,8 +231,6 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
-  | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism
-                                       on parameter universes has not been checked. *)
   | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =
diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v
deleted file mode 100644
index fbd9c8bcba..0000000000
--- a/test-suite/failure/Template.v
+++ /dev/null
@@ -1,28 +0,0 @@
-
-Module TestUnsetTemplateCheck.
-  Unset Template Check.
-
-  Section Foo.
-
-    Context (A : Type).
-
-    Definition cstr := nat : ltac:(let ty := type of A in exact ty).
-
-    Inductive myind :=
-    | cons : A -> myind.
-  End Foo.
-
-  (* Can only succeed if no template check is performed *)
-  Check myind True : Prop.
-
-  About myind.
-
-  (* test discharge puts things in the right order (by using the
-     checker on the result) *)
-  Section S.
-
-    Variables (A:Type) (a:A).
-    Inductive bb (B:Type) := BB : forall a', a = a' -> B -> bb B.
-  End S.
-
-End TestUnsetTemplateCheck.
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 7d919956e8..506a8dc5b0 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -32,10 +32,6 @@ let set_type_in_type () =
   let typing_flags = Environ.typing_flags (Global.env ()) in
   Global.set_typing_flags { typing_flags with Declarations.check_universes = false }
 
-let set_no_template_check () =
-  let typing_flags = Environ.typing_flags (Global.env ()) in
-  Global.set_typing_flags { typing_flags with Declarations.check_template = false }
-
 (******************************************************************************)
 
 type color = [`ON | `AUTO | `EMACS | `OFF]
@@ -526,7 +522,6 @@ let parse_args ~help ~init arglist : t * string list =
     |"-list-tags" -> set_query oval PrintTags
     |"-time" -> { oval with config = { oval.config with time = true }}
     |"-type-in-type" -> set_type_in_type (); oval
-    |"-no-template-check" -> set_no_template_check (); oval
     |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
     |"-where" -> set_query oval PrintWhere
     |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help)
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 051638d53c..6848862603 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -81,7 +81,6 @@ let print_usage_common co command =
 \n  -sprop-cumulative      make sort SProp cumulative with the rest of the hierarchy\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
-\n  -no-template-check     disable checking of universes constraints on universes parameterizing template polymorphic inductive types\
 \n  -mangle-names x        mangle auto-generated names using prefix x\
 \n  -set \"Foo Bar\"         enable Foo Bar (as Set Foo Bar. in a file)\
 \n  -set \"Foo Bar=value\"   set Foo Bar to value (value is interpreted according to Foo Bar's type)\
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index dacef1cb18..9f92eba729 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -356,8 +356,5 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
       in
-      if not mind.mind_typing_flags.check_template then
-        let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
-        ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu
-      else accu
+      accu
   in GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 8de1c69424..dce0a70f72 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -323,16 +323,15 @@ let check_named {CAst.loc;v=na} = match na with
   let msg = str "Parameters must be named." in
   user_err ?loc  msg
 
-let template_polymorphism_candidate ~template_check ~ctor_levels uctx params concl =
+let template_polymorphism_candidate ~ctor_levels uctx params concl =
   match uctx with
   | Entries.Monomorphic_entry uctx ->
     let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in
     if not concltemplate then false
-    else if not template_check then true
     else
       let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
       let params, conclunivs =
-        IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu
+        IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu
       in
       not (Univ.LSet.is_empty conclunivs)
   | Entries.Polymorphic_entry _ -> false
@@ -385,7 +384,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
           List.fold_left (fun levels c -> add_levels c levels)
             param_levels ctypes
         in
-        template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl
+        template_polymorphism_candidate ~ctor_levels uctx ctx_params concl
       in
       let template = match template with
         | Some template ->
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index cc104b3762..1286e4a5c3 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -76,17 +76,15 @@ val should_auto_template : Id.t -> bool -> bool
    inductive under consideration. *)
 
 val template_polymorphism_candidate
-  : template_check:bool
-  -> ctor_levels:Univ.LSet.t
+  : ctor_levels:Univ.LSet.t
   -> Entries.universes_entry
   -> Constr.rel_context
   -> Sorts.t option
   -> bool
-(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params
+(** [template_polymorphism_candidate ~ctor_levels uctx params
    conclsort] is [true] iff an inductive with params [params],
    conclusion [conclsort] and universe levels appearing in the
    constructor arguments [ctor_levels] would be definable as template
    polymorphic. It should have at least one universe in its
    monomorphic universe context that can be made parametric in its
-   conclusion sort, if one is given. If the [template_check] flag is
-   false we just check that the conclusion sort is not small. *)
+   conclusion sort, if one is given. *)
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 2cd1cf7c65..c9ce2d77fd 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -211,12 +211,10 @@ let pr_template_variables = function
 let print_polymorphism ref =
   let poly = Global.is_polymorphic ref in
   let template_poly = Global.is_template_polymorphic ref in
-  let template_checked = Global.is_template_checked ref in
   let template_variables = Global.get_template_polymorphic_variables ref in
   [ pr_global ref ++ str " is " ++
       (if poly then str "universe polymorphic"
        else if template_poly then
-         (if not template_checked then str "assumed " else mt()) ++
          str "template universe polymorphic "
          ++ h 0 (pr_template_variables template_variables)
        else str "not universe polymorphic") ]
diff --git a/vernac/record.ml b/vernac/record.ml
index df9b4a0914..f6945838d7 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -446,8 +446,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
                univs)
             param_levels fields
         in
-        let template_check = Environ.check_template (Global.env ()) in
-        ComInductive.template_polymorphism_candidate ~template_check ~ctor_levels univs params
+        ComInductive.template_polymorphism_candidate ~ctor_levels univs params
           (Some (Sorts.sort_of_univ min_univ))
       in
       match template with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d011fb2e77..60771e6ecf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -609,24 +609,6 @@ let vernac_assumption ~atts discharge kind l nl =
             | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
   ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
 
-let set_template_check b =
- let typing_flags = Environ.typing_flags (Global.env ()) in
- Global.set_typing_flags { typing_flags with Declarations.check_template = b }
-
-let is_template_check () =
-  let typing_flags = Environ.typing_flags (Global.env ()) in
-  typing_flags.Declarations.check_template
-
-let () =
-  let tccheck =
-    { optdepr = true;
-      optname = "Template universe check";
-      optkey = ["Template"; "Check"];
-      optread = (fun () -> is_template_check ());
-      optwrite = (fun b -> set_template_check b)}
-  in
-    declare_bool_option tccheck
-
 let is_polymorphic_inductive_cumulativity =
   declare_bool_option_and_ref ~depr:false ~value:false
     ~name:"Polymorphic inductive cumulativity"