Skip to Content.
Sympa Menu

coq-club - [Coq-Club] How can you know what does a tactic?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How can you know what does a tactic?


chronological Thread 
  • From: Romain Janvier <Romain.Janvier AT imag.fr>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] How can you know what does a tactic?
  • Date: Tue, 01 Jul 2003 12:33:46 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello.

I use tactics to proove some lemmas and I would like to know how I can obtain a script with every commands used by the tactics.
For example to proove "(P:Prop)P->P" you can use the "Auto" tactic.

If you save your proof you will optain the script:

"Auto"

What I would like to obtain is something like that:
"Intro P.
Assumption."

You can use "Info" to know what is done by a tactic, but only if it doesn't repeat itself. In this case, "Info" only gives the first comand used.

It should be possible because during a glimpse of Coq, I've obtain the list of commands made by a tactic.
If you interrupt the process during "Abstract tactic using subproof" during the saving process of "subproof" and you type "save." you can obtain the script of everything done by "tactic" to proove "subproof".

So the informations must be somewhere.

How can I obtain them without having to use the "abstract glimpse"?

Thank you.






Archive powered by MhonArc 2.6.16.

Top of Page