4 files changed, 25 insertions, 9 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/metasyntax.ml b/vernac/metasyntax.ml
index 4e79b50b79..3da12e7714 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1563,14 +1563,17 @@ let add_notation_extra_printing_rule df k v =
 
 (* Infix notations *)
 
-let inject_var x = CAst.make @@ CRef (qualid_of_ident (Id.of_string x),None)
+let inject_var x = CAst.make @@ CRef (qualid_of_ident x,None)
 
 let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
   check_infix_modifiers modifiers;
   (* check the precedence *)
-  let metas = [inject_var "x"; inject_var "y"] in
+  let vars = names_of_constr_expr pr in
+  let x = Namegen.next_ident_away (Id.of_string "x") vars in
+  let y = Namegen.next_ident_away (Id.of_string "y") vars in
+  let metas = [inject_var x; inject_var y] in
   let c = mkAppC (pr,metas) in
-  let df = CAst.make ?loc @@ "x "^(quote_notation_token inf)^" y" in
+  let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in
   add_notation local env c (df,modifiers) sc
 
 (**********************************************************************)
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;