From 51e8e857ee88a0c034dc74f69af2192ee51b2e35 Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Wed, 23 Apr 2014 17:32:28 +0200 Subject: Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q (refolding of cbn is smarter) --- theories/PArith/BinPosDef.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/PArith') 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. -- cgit v1.2.3