From e78b25709316ae9ed231034dd90d080872b991bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 8 Sep 2023 13:19:14 +0200 Subject: [PATCH] Better fix for coq/coq#17964: use correct direction of assumption instead of automatically generated name --- BigQ/QMake.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/BigQ/QMake.v b/BigQ/QMake.v index 950009e..cb8cfcb 100644 --- a/BigQ/QMake.v +++ b/BigQ/QMake.v @@ -226,7 +226,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. rewrite strong_spec_check_int. qsimpl. generalize (Zgcd_div_pos (ZZ.to_Z p) (NN.to_Z q)). lia. - rewrite e in *. + replace (NN.to_Z q) with 0%Z in * by (symmetry; assumption). rewrite Zdiv_0_l in *; auto with zarith. apply Zgcd_div_swap0; lia. (* Gt *)