diff options
| author | Hugo Herbelin | 2016-04-10 14:32:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:45 +0200 |
| commit | 9e9620b99f68622ebaf44c43e9945580f6cc6d98 (patch) | |
| tree | aa3c05f348b7520ccfe407db1301788a55f58673 /plugins | |
| parent | 973b6c69f0861c113f7bd5b94604d2497520a334 (diff) | |
So as to beautify to work, do not use notations in Inductive types
with a clause where, nor Notation, nor Fixpoints.
Should be certainly improved at least for Inductive types and
Fixpoints, depending on whether there is a "where" clause for
instance.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions