add missing nounfold for Qeq_bool in Sample.v

mit-plv · Nov 3, 2024 · edd0611 · edd0611
1 parent e4d987c
commit edd0611
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v b/src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v
@@ -60,7 +60,7 @@ Lemma continued_fraction_correct v n
   : eval_continued_fraction (continued_fraction v n) == v.
 Proof.
   cbv [eval_continued_fraction].
-  revert v; induction n; intro; cbn; destruct (Qeq_bool 0 v) eqn:H; cbn.
+  revert v; induction n; intro; cbn -[Qeq_bool]; case Qeq_bool eqn:H.
   all: rewrite ?Qeq_bool_iff in H; rewrite <- ?H.
   all: try reflexivity.
   { rewrite (surjective_pairing (continued_fraction _ _)); cbn.

diff --git a/src/Rewriter/Util/Strings/ParseArithmetic.v b/src/Rewriter/Util/Strings/ParseArithmetic.v
@@ -1,7 +1,7 @@
 From Coq Require Import Ascii String List.
 From Coq Require Import BinNums.
 From Coq Require Import QArith.
-From Coq Require Import BinInt.
+From Coq Require Import ZArith.
 Require Import Rewriter.Util.Option.
 From Coq Require BinaryString.
 From Coq Require OctalString.