diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-04-23 17:32:28 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-05-26 15:28:33 +0200 |
| commit | 51e8e857ee88a0c034dc74f69af2192ee51b2e35 (patch) | |
| tree | a440b661a946cd6f7d7a9f957da1344b6753fd38 /theories/PArith | |
| parent | 8ffd4e54ba8a05cb57f09d4333a7990f96a4cfd0 (diff) | |
Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q
(refolding of cbn is smarter)
Diffstat (limited to 'theories/PArith')
| -rw-r--r-- | theories/PArith/BinPosDef.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 22f3dcd64..fe1ec9398 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -268,7 +268,7 @@ Fixpoint compare_cont (r:comparison) (x y:positive) {struct y} : comparison := | 1, 1 => r end. -Definition compare x y := compare_cont Eq x y. +Definition compare := compare_cont Eq. Infix "?=" := compare (at level 70, no associativity) : positive_scope. |