diff options
| author | Hugo Herbelin | 2017-05-20 21:27:34 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 00:35:46 +0200 |
| commit | 9ee5808746cbcf6e04c08e6a2e798b6cbb34bb06 (patch) | |
| tree | 4304ee584c02cbee626dc1ace75e384faf990e4a /dev/doc | |
| parent | bcc9165aec1a80d563d7060ef127ad022e9ed008 (diff) | |
Fixing a too lax constraint for finding recursive binder part of a notation.
This was preventing to work examples such as:
Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions