The Coq mailing list

["Grant Jurgensen" <grant AT jurgensen.dev>]

Hi all,

I have been having trouble with higher-order Ltac and hoping someone here might be able to illuminate the issue or point me in the right direction. I have repeatedly run into unexpected behavior when passing Ltac to another tactic. My best guess is that I am misunderstanding when Ltac arguments are evaluated.

Here is an example:

```

Ltac hyp_eq H H' :=

  match H with

  | H' => idtac

  end.

Ltac revert_all_but H :=

  repeat (match goal with

  | H': _ |- _ =>

      assert_fails (hyp_eq H H');

      revert H'

  end).

Ltac revert_all_but2 H :=

  repeat (match goal with

  | H': _ |- _ =>

      assert_fails (idtac; hyp_eq H H');

      revert H'

  end).

Goal forall n m, n + m = m + n.

Proof.

  intros *.

  (* This one does nothing *)

  Fail progress revert_all_but m.

  (* This one acts as expected *)

  revert_all_but2 m.

Abort.

```

In this snippet, `revert_all_but H` is expected to revert all hypotheses except `H`. However, the real behavior is that it does nothing. The alternate tactic `revert_all_but2` adds an `idtac` statement to the Ltac passed to `assert_fails`, and somehow this manages to fix the problem.

I would have expected the two definitions to be equivalent, and I'm unsure why adding the `idtac` statement changes its behavior. My best guess is that in the original definition, the Ltac is executed before the function call in a call-by-value style, whereas in the second, it is essentially being called by name. Is this true? If so, why is some Ltac executed immediately, and some not?

Thanks,

Grant Jurgensen