diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-11 18:57:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-11 19:09:19 +0200 |
| commit | 9acfdfd9b7d1cae34b97a4c06c52c4646e15589b (patch) | |
| tree | c41decbdd8bb9eb81c076cdea6d1c64bbcb0ff94 /interp/notation_ops.ml | |
| parent | 16d0e6f7cfc453944874cc1665a0eb4db8ded354 (diff) | |
The grammar_extend function now registers unsynchronized extensions.
This made little sense, as all the uses of this function were actually
called from toplevel ML modules. This was at best useless, and at worst
a source of bugs when loading plugins and messing with backtracking.
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions