diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 16 | ||||
| -rw-r--r-- | vernac/comInductive.mli | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
3 files changed, 18 insertions, 2 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 7745f3eec7..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) @@ -425,7 +437,9 @@ let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations | Some template -> if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); template - | None -> not poly && Option.cata (fun s -> not (Sorts.is_small s)) false concl + | 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; diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index b523e9c014..8a2c9b8719 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -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 diff --git a/vernac/record.ml b/vernac/record.ml index 3e88489208..d36586d062 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -425,7 +425,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St template | None, template -> (* auto detect template *) - template && not poly && + ComInductive.should_auto_template () && template && not poly && let _, s = Reduction.dest_arity (Global.env()) arity in not (Sorts.is_small s) in |