I found an inconsistency in the behavior of the ssr rewrite provided by Coq and the one provided by MathComp. Is this a bug, and if so is it a Coq bug or a MathComp one? I don't know in which issue tracker to report this.

```
Variables (p q : bool).
Axiom H : p = true -> q = true.
(* Regular rewrite *)
Goal q = true.
rewrite H. (* side-condition appears last *)
Abort.
From Coq Require Import ssreflect.
(* ssr rewrite from Coq *)
Goal q = true.
rewrite H. (* side-condition appears first *)
Abort.
From mathcomp Require Import all_ssreflect.
(* ssr rewrite from mathcomp *)
Goal q = true.
rewrite H. (* side-condition appears last *)
Abort.
```

This is controlled by a flag (something like `SsrRewriteGoalOrder`

). I suppose that, if you only import `ssreflect`

, the flag does not get set and you get old behavior.

Oh, I see. So, to be clear, the old behavior is to show the side-condition first?

I am not so sure. I think this is the new behavior (or at least that is the one I would like). But for compatibility reasons, both vanilla Coq and full MathComp use the old behavior of having the side condition appear last.

```
From Coq Require Import ssreflect.
Set SsrOldRewriteGoalsOrder.
(* ssr rewrite from Coq *)
Goal q = true.
rewrite H. (* side-condition appears last *)
```

Yeah. Here is the doc for future reference.

Do you (does anyone) know whether there are plans to port MathComp to showing side-conditions first and unsetting that flag by default?

would be nice to have some tools that would make this kind of port semi-automatically

Last updated: Jun 25 2024 at 17:02 UTC