The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/31/2017 05:59 PM, Robert Rand wrote:
> Hi all,
>
> I'm trying to use Ltac to apply a tactic called type_check_once to all
> goals until no further progress can be made. Often this requires a cascade:
> type_check_once might instantiate a existential variable in goal #6 which
> then allows us to solve goal #3. No new goals are generated in this process.
>
> The problem is that the tactics seem to focus on a single goal, and does
> not cascade properly.
>
> In Coq 8.5 the following code worked but it fails in 8.6 (that is, we now
> have to call "all: type_check" multiple times in a row to solve all goals).
>
> Ltac type_check := let n := numgoals in do n type_check_once.
>
> (I've also tried using [> type_check_once..] in place of type_check, but
> this doesn't seem to buy us anything.)
>
> The following two approaches seemed to show promise, but both fail in some
> cases, for reasons unclear to me:
>
> Ltac type_check_num :=
>    let pre := numgoals in
>    type_check_once;
>    let post := numgoals in
>    tryif (guard post < pre) then type_check_num else idtac.
>
> Ltac type_check_circ :=
>    intros; compute;
>    try (progress [> type_check_once ..]; type_check_circ)
>
> Any suggestions?

Robert,

Have you tried:

Ltac type_check := let n := numgoals in do n repeat type_check_once.

You also might be interested in the lengthy discussion in 
https://coq.inria.fr/bugs/show_bug.cgi?id=3878

-- Jonathan