diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 15:27:10 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 15:27:10 +0200 |
commit | a3c40242a4786afd86cbfce7208e7b42b09c0863 (patch) | |
tree | af2ed94c35f780507e4fcf5ae1164c00e3a9923e /plugins/omega | |
parent | dcc5064bbc6f01b498abfdf80f0ea13a26381926 (diff) | |
parent | 256ca51bafc7200c8c006981cad60e57014e0dbc (diff) |
Merge PR#448: Do not recompute twice the whnf of terms in conversion.
Diffstat (limited to 'plugins/omega')
0 files changed, 0 insertions, 0 deletions