Add option to control automatic template polymorphism.

4 files changed, 32 insertions, 4 deletions

diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index a8fe1baa1b..1c6e2d81d8 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -1,6 +1,6 @@
 Set Printing Universes.
 
-Module Auto.
+Module AutoYes.
   Inductive Box (A:Type) : Type := box : A -> Box A.
 
   About Box.
@@ -10,7 +10,19 @@ Module Auto.
   Definition j_lebox (A:Type@{j}) := Box A.
   Definition box_lti A := Box A : Type@{i}.
 
-End Auto.
+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]
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