coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Hi,

Does anyone have a script to automatically indent a Coq *proof* ?

I would like to add curly brackets {} and bullets to an existing proof to group the tactics solving the same goal.

Cheers,

Julien Narboux

[Coq-Club] Automatic Indentation, Julien Narboux, 06/17/2014
- Re: [Coq-Club] Automatic Indentation, Bas Spitters, 06/18/2014
  - Re: [Coq-Club] Automatic Indentation, Eelis van der Weegen, 06/18/2014
    - Re: [Coq-Club] Automatic Indentation, Julien Narboux, 06/19/2014
      - Re: [Coq-Club] Automatic Indentation, Pierre Courtieu, 06/20/2014
        
        Re: [Coq-Club] Automatic Indentation, Julien Narboux, 06/20/2014
        
        Re: [Coq-Club] Automatic Indentation, Pierre Courtieu, 06/20/2014
        
        Re: [Coq-Club] Automatic Indentation, Strub, Pierre-Yves, 06/20/2014
        Re: [Coq-Club] Automatic Indentation, Pierre Courtieu, 06/23/2014
        Re: [Coq-Club] Automatic Indentation, Stefan Monnier, 06/23/2014
        
        Re: [Coq-Club] Automatic Indentation, Jonathan, 06/20/2014