diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-20 21:27:34 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-31 00:35:46 +0200 |
| commit | 9ee5808746cbcf6e04c08e6a2e798b6cbb34bb06 (patch) | |
| tree | 4304ee584c02cbee626dc1ace75e384faf990e4a /printing/ppconstr.mli | |
| 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 'printing/ppconstr.mli')
0 files changed, 0 insertions, 0 deletions