add missing nounfold for Qeq_bool in Sample.v (#48)

coq-community · Jan 4, 2025 · 0e14c7b · 0e14c7b
1 parent d9d85c8
commit 0e14c7b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/PerformanceExperiments/Sample.v b/PerformanceExperiments/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]; destruct (Qeq_bool 0 v) eqn:H; cbn.
   all: rewrite ?Qeq_bool_iff in H; rewrite <- ?H.
   all: try reflexivity.
   { rewrite (surjective_pairing (continued_fraction _ _)); cbn.