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