coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to determine the parameters order in "apply" tactic

From: xiang sen <xiangsen AT ustc.edu>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] How to determine the parameters order in "apply" tactic
Date: Sun, 03 Jul 2005 15:38:42 +0800
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi, all :

When I apply a lemma on the current goal , there are many parameters
required to be specified.
But their order seems puzzling. What 's the mechanism of order
determination in coq. Thanks!

All the best!
Xiang Sen

[Coq-Club] How to determine the parameters order in "apply" tactic, xiang sen
- Re: [Coq-Club] How to determine the parameters order in "apply" tactic, Pierre Casteran
  - Re: [Coq-Club] How to determine the parameters order in "apply" tactic, xiang sen
    - Re: [Coq-Club] How to determine the parameters order in "apply" tactic, anoun
      - Re: [Coq-Club] How to determine the parameters order in "apply" tactic, xiang sen
- <Possible follow-ups>
- Re: [Coq-Club] How to determine the parameters order in "apply" tactic, Yves Bertot