diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-10 14:32:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:43:27 +0200 |
| commit | 16b13e1aeac9559fc43939aa6d1d3f13a08daa14 (patch) | |
| tree | a8713e6018868ae599b001ac7dd462645fee5da3 /Makefile.build | |
| parent | c408cf73a6e170c7f4d3920427e4d4fdd4bef124 (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 'Makefile.build')
0 files changed, 0 insertions, 0 deletions