From b754d9a9a5f238cf2a30e50179a493a273b00830 Mon Sep 17 00:00:00 2001 From: nicolas tabareau Date: Mon, 20 Oct 2025 18:56:34 +0200 Subject: [PATCH] fix after #107 in bignums --- implementations/QType_rationals.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/implementations/QType_rationals.v b/implementations/QType_rationals.v index 9392351..829bdde 100644 --- a/implementations/QType_rationals.v +++ b/implementations/QType_rationals.v @@ -75,7 +75,7 @@ Proof. constructor; try apply _. intros x y. auto. Qed. #[global] Instance: SemiRing_Morphism to_Q. -Proof. repeat (constructor; try apply _); intros; qify; reflexivity. Qed. +Proof. repeat (constructor; try apply _); intros; qify; autorewrite with qsimpl; reflexivity. Qed. #[global] Instance inject_Q_QType: Cast Q t := of_Q.