From f34bf0434adbd527957e38710af654da6baec1e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 8 Sep 2023 11:45:12 +0200 Subject: [PATCH] Stop relying on `replace by` automatic `assumption`-based solving Before coq/coq#17964 `replace foo with bar by tac` actually means `replace foo with bar by first [assumption | symmetry; assumption | tac]`. --- BigQ/QMake.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/BigQ/QMake.v b/BigQ/QMake.v index e40df3d..950009e 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. - replace (NN.to_Z q) with 0%Z in * by assumption. + rewrite e in *. rewrite Zdiv_0_l in *; auto with zarith. apply Zgcd_div_swap0; lia. (* Gt *)