From 0e14c7b4475d5ea7c3a6aa416f4a761b0e9f8b2f Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 4 Jan 2025 09:35:53 -0500 Subject: [PATCH] add missing nounfold for Qeq_bool in Sample.v (#48) --- PerformanceExperiments/Sample.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PerformanceExperiments/Sample.v b/PerformanceExperiments/Sample.v index a5c4a8194a..9291d3ac83 100644 --- 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.