diff options
| author | Gaëtan Gilbert | 2019-11-20 16:27:09 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-20 16:27:09 +0100 |
| commit | 1248aed77ee36778cd440c14c4550dc97f78520b (patch) | |
| tree | 28a6ea3240a822fae58b5b5bc79b062247863fe7 /dev/doc/patch.ocaml-3.10.drop.rectypes | |
| parent | f37db0ff9b59720bb80433dff2995862550aec50 (diff) | |
make VernacArguments closer to user syntax
ie keep the fake arguments "/" and "&" instead of getting their index
at parsing time.
Diffstat (limited to 'dev/doc/patch.ocaml-3.10.drop.rectypes')
0 files changed, 0 insertions, 0 deletions