coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [LTac] Iteration on all hypothesis

From: Carlos Simpson <Carlos.Simpson AT unice.fr>
To: Adam Chlipala <adam AT chlipala.net>
Cc: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] [LTac] Iteration on all hypothesis
Date: Thu, 12 Aug 2010 03:32:28 +0200

Hi all,
Just as a general remark, wouldn't it be good to start heading towards a
more complete and general version of Ltac, say one which would get in trouble
with the Neuromancer's "Turing police"?
---Carlos Simpson

[Coq-Club] [LTac] Iteration on all hypothesis, Alexandre Pilkiewicz
- Re: [Coq-Club] [LTac] Iteration on all hypothesis, Adam Chlipala
  - Re: [Coq-Club] [LTac] Iteration on all hypothesis, Alexandre Pilkiewicz
    - Re: [Coq-Club] [LTac] Iteration on all hypothesis, Adam Chlipala
      - Re: [Coq-Club] [LTac] Iteration on all hypothesis, Carlos Simpson
- Re: [Coq-Club] [LTac] Iteration on all hypothesis, Eric Jaeger