Karl Palmskog

You can remove the other shield by setting `community: false`.

To replicate, install MathComp SSReflect and clone and build the repo: ```shell $ opam repo add coq-released https://coq.inria.fr/opam/released $ opam pin add coq-mathcomp-ssreflect 1.9.0 $ git clone https://github.com/coq-community/reglang.git $ cd...

@JulesViennotFranca this may be due to some interaction with Equations. But can you please post a self-contained minimal example that recreates the error on current AAC Tactics? For example you,...

@aa755 I just maintain this project, and unfortunately have no plans to extend it with new tactics (but a PR implementing `aac_congruence` would be welcome). Someone who may be able...

Thanks Damien, I will leave this issue open since there is still the possibility of `aac_congruence` happening. Just to double check also @aa755, you know about the `aac_normalise` tactic, right?

@damien-pous I think if the changes in the branch canonical-ordering fits the needs of @aa755, we should do two things: - merge those changes into the `v8.19` branch and make...

Then it seems we all agree on a new release. @aa755 can I include your `gcd` example and instances into the tutorial? @damien-pous I assume I can take it from...

@damien-pous thanks, I will likely do the release by tomorrow, so no chance of duplicated effort yet.

Release with `aac_normalise` changes is done and submitted as opam package: https://github.com/coq/opam/pull/3040 I think we keep this issue open to track any progress on aac_congruence that might happen, so I...

@clayrat OK by you to merge this? The main upside is avoiding a bunch of warnings (and hopefully getting Rocq compatibility for free).