diff options
| author | Gaëtan Gilbert | 2019-01-04 09:12:03 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-04 09:12:03 +0100 |
| commit | 246012c65aff12bae347be57b0432128a593c72a (patch) | |
| tree | 294616dc2236ec38fae84e0a3b173bd3d694ef50 | |
| parent | 0a5bbf347b5bbcb579f94eb3d0166778cd92cfdb (diff) | |
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.
| -rw-r--r-- | vernac/comInductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 " ++ |