coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] local definition in proof mode

From: andr� hirschowitz <ah AT unice.fr>
To: Martijn Vermaat <martijn AT vermaat.name>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] local definition in proof mode
Date: Tue, 6 Apr 2010 13:22:20 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=paC4nWTc244UerXepm9Zw6lItWa48lhvy6lFguo1gN24QyYshxtLu0RFLDw8lY/BlT sz92gkkUnOiZ+wLJvuGGrZfo3XUtYXyMVEyqju8RfVaE+IfuCqxj+SyxMNK3kNt+GGDr diHfqr+DG3itx5xte8pmgNrfwV8oAO5CkTWO4=

no, if I experiment correctly.

assert generates two goals and does not forward to the second one the formula produced for the first one.

Thanks for your answer.

ah

I think you are looking for the following?

�assert (myname : mytype).

[Coq-Club] local definition in proof mode, andr� hirschowitz
- Re: [Coq-Club] local definition in proof mode, Martijn Vermaat
  - Re: [Coq-Club] local definition in proof mode, andr� hirschowitz
    - Re: [Coq-Club] local definition in proof mode, St�phane Lescuyer
      - Re: [Coq-Club] local definition in proof mode, Guillaume Allais
        
        Re: [Coq-Club] local definition in proof mode, Pierre-Marie P�drot
      - Re: [Coq-Club] local definition in proof mode, Jean-Francois Monin
        
        Re: [Coq-Club] local definition in proof mode, AUGER
      - Re: [Coq-Club] local definition in proof mode, AUGER
        
        Re: [Coq-Club] local definition in proof mode, andr� hirschowitz
        
        Re: [Coq-Club] local definition in proof mode, Jean-Francois Monin
        
        Re: [Coq-Club] local definition in proof mode, AUGER
        
        Re: [Coq-Club] local definition in proof mode, Pierre-Marie Pédrot