diff options
| author | Gaëtan Gilbert | 2018-09-17 11:14:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-19 17:02:45 +0100 |
| commit | 0a25e351d6a2d25e5d82b165843a09a2804fadc6 (patch) | |
| tree | 1f0817b904f92b8a69b4d2d91d624cab5734a818 | |
| parent | a616310f3896091982518772f59b9f9a8540e1d2 (diff) | |
Add CHANGES for auto-template warning.
| -rw-r--r-- | CHANGES.md | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/CHANGES.md b/CHANGES.md index d64b5accd7..b8c0068778 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -135,6 +135,17 @@ Universes for the "Private Polymorphic Universes" option (and Unset it to get the previous behaviour). +Inductives + +- An option and attributes to control the automatic decision to + declare an inductive type as template polymorphic were added. + Warning "auto-template" will trigger when an inductive is + automatically declared template polymorphic without the attribute. + +Funind + +- Inductive types declared by Funind will never be template polymorphic. + Misc - Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances. |