diff options
| author | Pierre Boutillier | 2014-04-23 17:32:28 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-05-26 15:28:33 +0200 |
| commit | 51e8e857ee88a0c034dc74f69af2192ee51b2e35 (patch) | |
| tree | a440b661a946cd6f7d7a9f957da1344b6753fd38 /kernel/reduction.ml | |
| parent | 8ffd4e54ba8a05cb57f09d4333a7990f96a4cfd0 (diff) | |
Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q
(refolding of cbn is smarter)
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions