The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Fri, Feb 15, 2008 at 02:47:21PM +0100, Birgit Fruth wrote:
> 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!

Having never used cofix, would this work?

  let H := fresh in cofix H ; ...

Edsko