coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to hide section context?

From: Jacek Chrzaszcz <chrzaszc AT mimuw.edu.pl>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] How to hide section context?
Date: Wed, 14 Aug 2002 17:54:55 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello everybody,

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...

Thank you

Jacek Chrzaszcz

[Coq-Club] How to hide section context?, Jacek Chrzaszcz
- Re: [Coq-Club] How to hide section context?, Hugo Herbelin