aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checkInductive.ml1
-rw-r--r--checker/check_stat.ml8
-rw-r--r--checker/values.ml2
-rw-r--r--kernel/cooking.ml18
-rw-r--r--kernel/declarations.ml4
-rw-r--r--kernel/declareops.ml1
-rw-r--r--kernel/environ.ml16
-rw-r--r--kernel/environ.mli3
-rw-r--r--kernel/indTyping.ml17
-rw-r--r--kernel/indTyping.mli1
-rw-r--r--library/global.ml2
-rw-r--r--library/global.mli1
-rw-r--r--printing/printer.ml8
-rw-r--r--printing/printer.mli2
-rw-r--r--test-suite/failure/Template.v28
-rw-r--r--toplevel/coqargs.ml5
-rw-r--r--toplevel/usage.ml1
-rw-r--r--vernac/assumptions.ml5
-rw-r--r--vernac/comInductive.ml7
-rw-r--r--vernac/comInductive.mli8
-rw-r--r--vernac/prettyp.ml2
-rw-r--r--vernac/record.ml3
-rw-r--r--vernac/vernacentries.ml18
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"
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:16:21 +0000