The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 23/04/2012 16:08, Valentin ROBERT a écrit :
> So I should rephrase my thought into: it seemed to do what I expected
> sometimes (that is, work quite like if I had used a tactic notation
> with constr(...)), but it also did something I did not expect to
> happen (that is, accept match_args_A foo bar where foo and bar don't
> exist). Now, I do not understand why I can pass these parameters,
> while the behavior does not seem to depend on what I pass in.

I think foo and bar are here interpreted as raw identifiers. For
example, you can do:

  Ltac intro2 x := intro x.
  Theorem test: forall (rs: nat) r, rs = r -> True.
  Proof.
    intro2 rs.
  [...]

The constr(...) in Tactic Notation forces ... to be a valid constr
(hence, to exist).

I suggest you expose your tactic to users as a Tactic Notation that
forces constr(...). You can define recursively your tactic using Ltac,
and force the type of the argument in recursive calls, as in:

  Ltac mytac_internal x :=
    [...]
    mytac_internal (constr:...).
  Tactic Notation "mytac" constr(x) := mytac_internal x.


Cheers,

-- 
Stéphane