Skip to content

Commit

Permalink
Adapt to Coq PR #17832: syntax of choice in rewstrategy expects argum…
Browse files Browse the repository at this point in the history
…ents at atomic level.

There are spaces in "( <- associativity )" to prevent the notation "(< x )" to be parsed.
  • Loading branch information
herbelin committed Nov 4, 2023
1 parent 6ad1db9 commit e6ac96a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion theory/groups.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down

0 comments on commit e6ac96a

Please sign in to comment.