coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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/
- [Coq-Club] cofix with automatic names, Birgit Fruth
- Re: [Coq-Club] cofix with automatic names, Edsko de Vries
Archive powered by MhonArc 2.6.16.