coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to match several hypo. in Ltac

From: Pierre Casteran <pierre.casteran AT labri.fr>
To: xiang sen <xiangsen AT ustc.edu>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] How to match several hypo. in Ltac
Date: Mon, 27 Jun 2005 13:39:08 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

Selon xiang sen
<xiangsen AT ustc.edu>:

> Thanks a lot!
> By the way, the pattern described in Page 203 of Coq art should be
> corrected, shouldn't it?
>

which one ?

In my electronic version, I found :

[h1 : t1; h2 : t2 ... |- C] => tac

which seems to be OK.

Pierre

> Best regards
>
> Sen
>

--
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

[Coq-Club] How to match several hypo. in Ltac, xiang sen
- Re: [Coq-Club] How to match several hypo. in Ltac, Pierre Casteran
  - Re: [Coq-Club] How to match several hypo. in Ltac, Pierre Casteran
    - Re: [Coq-Club] How to match several hypo. in Ltac, xiang sen
      - Re: [Coq-Club] How to match several hypo. in Ltac, Pierre Casteran
        
        Re: [Coq-Club] How to match several hypo. in Ltac, xiang sen
        
        Re: [Coq-Club] How to match several hypo. in Ltac, Pierre Casteran