Skip to Content.
Sympa Menu

coq-club - [Coq-Club] cofix with automatic names

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] cofix with automatic names


chronological Thread 
  • From: "Birgit Fruth" <birgit AT fruth.org>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] cofix with automatic names
  • Date: Fri, 15 Feb 2008 14:47:21 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi!
I want do prove something and I have to do this of cofix and other tactics very often. So I tried to put it into a repeat but cofix always tries to use the same name again and again.
There is an error: User error: name already used in the environment.

What can I do?

repeat( cofix; ...).

instead of

cofix H8.
rewrite autotree_unfold;simpl;apply Always_every;try(trivial || (apply (Atomic_tree_intrld safe;tauto) || (apply Always_leafs)).
cofix H9.
rewrite autotree_unfold;simpl;apply Always_every;try((trivial) || (apply (Atomic_tree_intro K1);simpl;unfold safe;tauto )|| (apply Always_leafs)).
...

Thanks for your help!

Birgit
--
Erstellt mit Operas revolutionärem E-Mail-Modul: http://www.opera.com/mail/





Archive powered by MhonArc 2.6.16.

Top of Page