Hi! In my proofs, I often get a large number of variables with some similar types. If they are quantified together, Coq will merge them into `a, c : T1`

. If not, they will get 2 different lines: `a:T1 ... b:T1`

. Is there a way to clean (factorize?) a proof state to improve readability? (especially, compactness)

Here is a minimal example:

```
Parameter T1 T2 :Type.
Lemma my_lemma: forall (a:T1) (b:T2) (c:T1) (d:T2), False.
Proof.
intros.
(* factorize proof state to get :
a, c : T1
b, d : T2 *)
Admitted.
```

I'm here interested in the case where of course b does not appear in c's type.

Thanks a lot !

You have `move`

tactics to do this manually: https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.move

I don't know if there is something automatic.

Thanks ! That's a starting point, I'm trying out some ltac to see if I can get it to move all variables of the same type to the top...

Last updated: Sep 26 2023 at 12:02 UTC