Merge PR #8488: Warning when using automatic template polymorphism

3 files changed, 19 insertions, 6 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 4af6415a4d..348e76da62 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -34,6 +34,13 @@ module RelDecl = Context.Rel.Declaration
 
 (* 3b| Mutual inductive definitions *)
 
+let warn_auto_template =
+  CWarnings.create ~name:"auto-template" ~category:"vernacular"
+    (fun id ->
+       Pp.(strbrk "Automatically declaring " ++ Id.print id ++
+           strbrk " as template polymorphic. Use attributes or " ++
+           strbrk "disable Auto Template Polymorphism to avoid this warning."))
+
 let should_auto_template =
   let open Goptions in
   let auto = ref true in
@@ -44,7 +51,10 @@ let should_auto_template =
         optread  = (fun () -> !auto);
         optwrite = (fun b -> auto := b); }
   in
-  fun () -> !auto
+  fun id would_auto ->
+    let b = !auto && would_auto in
+    if b then warn_auto_template id;
+    b
 
 let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
   | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
@@ -431,8 +441,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
           if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
           template
         | None ->
-          should_auto_template () && not poly &&
-          Option.cata (fun s -> not (Sorts.is_small s)) false concl
+          should_auto_template ind.ind_name (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 9df8f7c341..1d6f652385 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -46,7 +46,10 @@ val declare_mutual_inductive_with_eliminations :
   mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
   MutInd.t
 
-val should_auto_template : unit -> bool
+val should_auto_template : Id.t -> bool -> bool
+(** [should_auto_template x b] is [true] when [b] is [true] and we
+   automatically use template polymorphism. [x] is the name of the
+   inductive under consideration. *)
 
 (** Exported for Funind *)
 
diff --git a/vernac/record.ml b/vernac/record.ml
index ffd4f654c6..2867ad1437 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -415,9 +415,9 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
         template
       | None, template ->
         (* auto detect template *)
-        ComInductive.should_auto_template () && template && not poly &&
+        ComInductive.should_auto_template id (template && not poly &&
         let _, s = Reduction.dest_arity (Global.env()) arity in
-        not (Sorts.is_small s)
+        not (Sorts.is_small s))
     in
     { mind_entry_typename = id;
       mind_entry_arity = arity;