diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-21 11:24:21 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-21 11:24:21 -0400 |
| commit | e5ff8aac93faf465510bb4eb143db714e9c80813 (patch) | |
| tree | e31fd750deea4cd9fc0a4cdcdaef9ea188bfe789 /src | |
| parent | 19b850574a479ccd7984b584d89e67513d719a01 (diff) | |
Fixes #29
Diffstat (limited to 'src')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 3 |
1 files changed, 1 insertions, 2 deletions
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. |