The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Brian Aydemir wrote:
> I have a question about solving obligations generated by Program 
> Fixpoint in the current svn snapshot of Coq 8.2 (r11354). I'm using 
> the documentation at http://coq.inria.fr/V8.2beta4/doc/refman/html/ . 
> Consider the following silly and trivial example. (There's no reason 
> to do this in practice, but it does illustrate my problem.)

It's hard to tell which features of [Program] you are using, since your 
example is implementable trivially with normal [Fixpoint]. For my own 
edification, can you explain why you are using [Program] instead of 
[refine]? Your problem is a non-issue with [refine], since you simply 
run [refine implementation; your_default_tactic] in the proof script for 
the function you're writing.