The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Quoting Adam Chlipala 
<adam AT chlipala.net>:
----------------------------

> You never need to use tactics to write anything in Coq.  I recommend  
> avoiding tactics for anything that you think of as a "program," and  
> using tactics for anything you think of as a "proof."

If you look at the script we proposed, the function we defined was an  
auxiliary
function for proving some theorem. So, I think it was it was  "a part  
of a proof".

Pierre