From 246012c65aff12bae347be57b0432128a593c72a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 4 Jan 2019 09:12:03 +0100
Subject: Default disable auto template warning.

The situation is too unclear to make it of general use, plus it has
some issues (#9296)
I'm not deleting the warning as it can still be useful to find which
types are template for those who want to experiment.
---
 vernac/comInductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 348e76da62..25a4804743 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -35,7 +35,7 @@ module RelDecl = Context.Rel.Declaration
 (* 3b| Mutual inductive definitions *)
 
 let warn_auto_template =
-  CWarnings.create ~name:"auto-template" ~category:"vernacular"
+  CWarnings.create ~name:"auto-template" ~category:"vernacular" ~default:CWarnings.Disabled
     (fun id ->
        Pp.(strbrk "Automatically declaring " ++ Id.print id ++
            strbrk " as template polymorphic. Use attributes or " ++
-- 
cgit v1.2.3