From 3c888a6584b8872f179782a9a2b2d07f9b7076f1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 10 Aug 2016 11:54:27 -0700 Subject: 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]). --- src/ModularArithmetic/BarrettReduction/ZBounded.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. -- cgit v1.2.3