The Coq mailing list

[Valentin ROBERT <valentin.robert.42 AT gmail.com>]

Thanks, the solution combining Ltac and Tactic Notation solves my issue.

Best regards,
- Valentin Robert

On Mon, Apr 23, 2012 at 16:35, Stéphane Glondu 
<steph AT glondu.net>
 wrote:
> 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