The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

AUGER Cédric wrote:
> Le Mon, 19 Dec 2011 09:20:02 -0500,
> Adam 
> Chlipala<adamc AT csail.mit.edu>
>   a écrit :
>    
> > My advice is this: never write program code with tactics (e.g., as
> > you're doing for [add] here).  Many people on this list will disagree
> > with that advice, but I believe tactics are a proper fit for "proofs"
> > only.  For an introduction to the techniques you'll need to avoid
> > using tactics to define [add] and similar functions, see CPDT:
> >       http://adam.chlipala.net/cpdt/
> >
> >      
> Adam, does the refine tactic falls in the "never write program code
> with tactics"?
>    

No, that pattern is consistent with what I meant.  I wasn't fully 
precise, but my suggestion was to write all executable code explicitly, 
which is completely compatible with passing that code as the argument to 
[refine].