Remove the Template Check option.

6 files changed, 8 insertions, 35 deletions

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"