aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-02-20 20:39:27 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-05 13:42:01 +0100
commit0b1032f2acdb6f7d92c84ba3afcbf3818cc107a9 (patch)
treed9ba31a2560c3f3d51db15ad22cd16bcab724357 /config
parent15331729aaab16678c2f7e29dd391f72df53d76e (diff)
[ssreflect] Export parsing witnesses in mli file.
This is needed in order to manipulate/serialize SSR's AST. A quicker [and maybe better] alternative would be to just remove `ssrparser.mli`, as there are many grammar entries that still need exporting.
Diffstat (limited to 'config')
0 files changed, 0 insertions, 0 deletions