From e6ac96ac6318772ad3c5199bef113f0fac2e321f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 4 Nov 2023 00:35:47 +0100 Subject: [PATCH] Adapt to Coq PR #17832: syntax of choice in rewstrategy expects arguments at atomic level. There are spaces in "( <- associativity )" to prevent the notation "(< x )" to be parsed. --- theory/groups.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theory/groups.v b/theory/groups.v index 8465585..05f9bb2 100644 --- a/theory/groups.v +++ b/theory/groups.v @@ -20,7 +20,7 @@ End semigroup_props. Ltac group_simplify := rewrite_strat (try bottomup (hints group_simplify)); - (try bottomup (choice (hints group_cancellation) <- associativity)). + (try bottomup (choice (hints group_cancellation) ( <- associativity ))). Ltac group := group_simplify; easy.