diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-15 21:44:32 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-20 20:19:45 +0100 |
commit | ab7fd497575b161eeb9bfe89da743b3fbc93aaf3 (patch) | |
tree | 4f95d0ae3300db7fd8aadd2406b203ec46226506 /tactics/hipattern.ml | |
parent | 2a857da2a88855a6c9f0fa7e48a8700c1613e0c7 (diff) |
Fixing factorization of recursive notations in the case of an atomic separator.
This addresses a limitation found in math-comp seq.v file. See the example in
test suite file success/Notations2.v.
To go further and accept recursive notations with a separator made of
several tokens, and assuming camlp5 unchanged, one would need to
declare an auxiliary entry for this sequence of tokens and use it as
an "atomic" (non-terminal) separator. See PR #6167 for details.
Diffstat (limited to 'tactics/hipattern.ml')
0 files changed, 0 insertions, 0 deletions