From 4bd2596b91fb48e0f9e26d6f7407327d7afab954 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 11 Sep 2023 22:31:50 +0200 Subject: [PATCH] Stop relying on `replace by` automatic `assumption`-based solving (#1657) Before coq/coq#17964 `replace foo with bar by tac` actually means `replace foo with bar by first [assumption | symmetry; assumption | tac]`. --- src/Fancy/Prod.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Fancy/Prod.v b/src/Fancy/Prod.v index 45df4844b3..f421bab684 100644 --- a/src/Fancy/Prod.v +++ b/src/Fancy/Prod.v @@ -114,7 +114,7 @@ Ltac step_rhs := match goal with | H: ?x = spec ?i ?args _ |- context [spec ?i ?args ?cc] => - replace (spec i args cc) with x by idtac + replace (spec i args cc) with x by first [assumption | symmetry;assumption] end; match goal with | H : ?y = (?x mod ?m)%Z |- context [(?x mod ?m)%Z] => @@ -397,4 +397,4 @@ Ltac push_value_unused := | _ => apply not_in_cons; split; [ try assumption; symmetry; assumption | ] | _ => apply in_nil - end. \ No newline at end of file + end.