diff options
| author | Hugo Herbelin | 2017-08-12 18:54:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-12 20:30:11 +0200 |
| commit | 5d3d60e88f137183b4155bfa446dc7f3ebb35993 (patch) | |
| tree | 47b14bce769ce243310173d8abf8033619d34592 /dev/include | |
| parent | a267b06c4a237ce3e4ce257e47f6429543804baa (diff) | |
Fixing a bug of recursive notations introduced in dfdaf4de.
When a proper notation variable occurred only in a recursive pattern
of the notation, the notation was wrongly considered non printable due
(the side effect that function compare_glob_constr and that
mk_glob_constr_eq does not do anymore was indeed done by aux' but
thrown away). This fixes it.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions