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/printer.ml | |
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/printer.ml')
0 files changed, 0 insertions, 0 deletions