From e5ff8aac93faf465510bb4eb143db714e9c80813 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 21 Jul 2016 11:24:21 -0400 Subject: Fixes #29 --- src/ModularArithmetic/ModularBaseSystemOpt.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'src') diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 4543ff67d..ed8f80659 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -194,8 +194,7 @@ Section Carries. let RHSf := match (eval pattern (nth_default_opt 0%Z (to_list _ b) i) in RHS) with ?RHSf _ => RHSf end in change (LHS = Let_In (nth_default_opt 0%Z (to_list _ b) i) RHSf). change Z.shiftl with Z_shiftl_opt. - change (-1) with (Z_opp_opt 1). - change Z.add with Z_add_opt at 5 9 17 21. + match goal with |- appcontext[ ?x + -1] => change (x + -1) with (Z_add_opt x (Z_opp_opt 1)) end. reflexivity. Defined. -- cgit v1.2.3