The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Jacek,
 
> Is it possible to ask coq not to display the section context during the
> proof? For example:
> 
> Section A.
> 
>   Local p:(P O).
>     (* big and ugly proof *)
>   Save.
> 
>   Lemma z : (x:nat)(x=O) -> (P O).
> 
> subgoal 1 is:
> 
>   p := (* big and ugly proof *) : (P O)
>   ============================
>    (x:nat)(x=O) -> (P O)
> 
> 
> I do not want to see p (and especially its body) here...

  In this case, you could do "ClearBody p". But if your question is
about hiding the whole section context in one step, nothing exists for
this to my knowledge. Please go ahead.

  Hugo