diff options
author | 2017-10-06 12:33:17 +0200 | |
---|---|---|
committer | 2017-10-06 12:33:17 +0200 | |
commit | fb45ec112ebdf6f18143b844e317a555f14e3b74 (patch) | |
tree | 3177e9781caff6d34c0ff6fc4536e8b0d59aa37c /plugins/extraction/scheme.mli | |
parent | 6bfa989253a3ec5563b07c5b14661d6b8dfebd6b (diff) | |
parent | c5aca4005faf74d99091ef29257cbed6a53a12d4 (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