The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

> First, is "Obligations Tactic" supposed to parse?  How else might I  
> set the default tactic to be applied to generated obligations?
>
> Second, why does Solve All Obligations not do anything?  The tactic  
> I've provided it works when I step through the obligations by hand.
>
> At a higher level, I want some way of telling Coq how to solve all  
> generated obligations.  The documentation suggests that this is  
> implemented and code in the standard library seems to use this  
> feature, so I'm confused by my own experience here.

Hi,

This is mainly a result of unsynchronized documentation and  
implementation. In
the trunk (including the doc), "Obligations Tactic" was renamed to  
"Obligation Tactic"
as I was advised of the better spelling. Then, you have to know that  
Solve Obligations
uses solely the tactic you give to solve the goal, and does not apply  
the default tactic
"program_simpl" before calling it, which can considerably simplify the  
goal and
always does [intros]. So, the following works:

<< Obligation Tactic := program_simpl ; simpl ; omega. >>

Cheers,
-- Matthieu