diff options
| author | Hugo Herbelin | 2016-03-28 15:01:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-03-28 15:01:05 +0200 |
| commit | 111e5edfe388d2f41ddef11800dac55b060b280b (patch) | |
| tree | 00ba7f2fccd5984cd83fb69da7ec1db77fd34368 /plugins/syntax/string_syntax.ml | |
| parent | d0a2ea9c4a68c33753c75cc80e4b255366c6352b (diff) | |
Was too restrictive in syntactic definitions, not imagining that they
could be used with arguments which are binding variables, as was done
in ssrfun.v.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions