diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-10 11:54:27 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-10 13:11:27 -0700 |
| commit | 3c888a6584b8872f179782a9a2b2d07f9b7076f1 (patch) | |
| tree | 15669287e6b4ee9cfca92a7e0976eb0caccec544 /src/ModularArithmetic/BarrettReduction/ZBounded.v | |
| parent | 3da2a1ce9d25da66f2f317dea68179b96bc71849 (diff) | |
Work around bug #4165 (broken context) in 8.4
This is https://coq.inria.fr/bugs/show_bug.cgi?id=4165, context
replacement is broken (in the presence of [let]).
Diffstat (limited to 'src/ModularArithmetic/BarrettReduction/ZBounded.v')
| -rw-r--r-- | src/ModularArithmetic/BarrettReduction/ZBounded.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/BarrettReduction/ZBounded.v b/src/ModularArithmetic/BarrettReduction/ZBounded.v index bcebd6ea7..0c4142573 100644 --- a/src/ModularArithmetic/BarrettReduction/ZBounded.v +++ b/src/ModularArithmetic/BarrettReduction/ZBounded.v @@ -42,7 +42,7 @@ Section barrett. assert ((decode_large x) mod b^(k-offset) < b^(k-offset)) by auto with zarith omega. rewrite (barrett_reduction_small m b (decode_large x) k μ offset) by omega. rewrite <- μ'_eq. - pull_zlike_decode. + pull_zlike_decode; cbv zeta; pull_zlike_decode. (* Extra [cbv iota; pull_zlike_decode] to work around bug #4165 (https://coq.inria.fr/bugs/show_bug.cgi?id=4165) in 8.4 *) subst pr; split; [ reflexivity | exact _ ]. Defined. End barrett. |