Merge pull request #122 from herbelin/master+adapting-coq-pr17832-cho…

…ice-stronger-precedence-rewstrategy Adapt to Coq PR #17832: syntax of choice in rewstrategy expects arguments at atomic level
coq-community · Nov 6, 2023 · f9712ba · f9712ba
2 parents 6ad1db9 + e6ac96a
commit f9712ba
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.