Ssreflect Users Discussion List

[<>]

Hello.

Could first and last tactical unfortunately interact with proof by 
coinduction?

I have been correcting my proof to get rid of unguarded recursive calls
and suspect  a tactic;
have [h | h] := "something..."; last first 
of making the unguarded call. 

kind regards,
Keiko