Automatic indenting for Easycrypt

[Adamw1NCSC]

Suggestion, rather than a bug/issue:

We've been using PG with Easycrypt for several months now, and are starting to think of a style guide. This has led to us thinking about internal guidance for indentation to make proofs easier to follow and navigate. Currently, there is no automatic indentation for Easycrypt, but we think there is a natural default. When new goals are generated as a result of executing a tactic, increase the indentation by one unit (tab, double space, whatever). Once all those goals are discharged, revert to prior level of indentation. This seems natural and would be extremely useful for understanding proof progression. This seems like it would be relatively simple to automate in Proof General, and would hugely improve the readability of the proofs.

[Matafou]

This sounds like a good idea, althoug in other provers (like coq) the indentation of proof script is better done using script structure itself, i.e. script bulleting and parenthesizing. Like this:

intro x y h.
induction H.
- auto. (* other goals at this point will necessitate the same bullet *) 
- destruct H0.
  { intuition. }  (* needs to be closed by "}" when the goal is finished. Next goal may not have bullet or bracket *)
  rewrite H2.
  auto.

So here the good feature would be to suggest (or auto insert) the right bullets

That said I am not sure someone will have time for this in the near future. PR welcome!