aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/scheme.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-06 12:33:17 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-06 12:33:17 +0200
commitfb45ec112ebdf6f18143b844e317a555f14e3b74 (patch)
tree3177e9781caff6d34c0ff6fc4536e8b0d59aa37c /plugins/extraction/scheme.mli
parent6bfa989253a3ec5563b07c5b14661d6b8dfebd6b (diff)
parentc5aca4005faf74d99091ef29257cbed6a53a12d4 (diff)
Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly BZ#4852)
Diffstat (limited to 'plugins/extraction/scheme.mli')
0 files changed, 0 insertions, 0 deletions