aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/extraction.mli
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-02-17 14:32:50 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-01-11 09:49:32 +0100
commitd15d8cc0ce584a6d80d878faf84314c6712ccf69 (patch)
tree0042925526cfd801451cdbe5472f44cd2169a57c /plugins/extraction/extraction.mli
parentb858f939f33dc4bc4c8e470ed62310ef15c59a99 (diff)
Extraction: minor tweaks to ease ongoing experiments about Lambda
- Common.get_native_char instead of just a pp function of this char - Enrich the record projection table
Diffstat (limited to 'plugins/extraction/extraction.mli')
0 files changed, 0 insertions, 0 deletions