diff options
| author | Maxime Dénès | 2019-01-21 10:21:43 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-21 10:21:43 +0100 |
| commit | 05e2222e04323d11429d659b415750cf40e2babd (patch) | |
| tree | a8bd88bc63965b6e2c919b02c62516b3b332c037 | |
| parent | d4f1225d059eb858a6d8430d2f86057ce7bb0c5c (diff) | |
| parent | 55b8347e758e86ca34aafaa635d48492c812bc3d (diff) | |
Merge PR #9304: Default disable auto template warning.
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
| -rw-r--r-- | doc/sphinx/language/cic.rst | 6 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 2 |
2 files changed, 7 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index cc5d9d6205..693ee28a47 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1041,6 +1041,12 @@ in :math:`\Type`. enabled it will prevail over automatic template polymorphism and cause an error when using the ``template`` attribute. +.. warn:: Automatically declaring @ident as template polymorphic. + + Warning ``auto-template`` can be used to find which types are + implicitly declared template polymorphic by :flag:`Auto Template + Polymorphism`. + If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local 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 " ++ |