The Coq mailing list

["Birgit Fruth" <birgit AT fruth.org>]

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/