The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Dear all

For those who might be interested, the solution to pass a tactic still
expecting arguments to a tactic defined by an EXTEND clause can be
found in the quote plugin, at the start of the g_quote.ml4 file:

let make_cont k x =
  let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> fst k)) in
  let x = TacDynamic(dummy_loc, Pretyping.constr_in x) in
  let tac = <:tactic<let cont := $k in cont $x>> in
  Tacinterp.interp tac

Tanks to Stéphane Glondu for pointing this out to me!

My apply' tactic now fully works with "with bindings", and properly
tag all remaining subgoals. Constructor' does the same.

Cheers

Alexandre Pilkiewicz


2010/12/13 Alexandre Pilkiewicz 
<alexandre.pilkiewicz AT polytechnique.org>:
> Dear list
>
> I wrote an apply' tactic that behaves as apply, except it tags each
> subgoal with the name of the corresponding hypothesis of the lemma
> (see here 
> https://github.com/pilki/cases/blob/master/test-suite/case_tactics_ex.v#L196
> to see what I mean)
>
> I would like not to extend it with "with bindings". I wrote everything
> I need on the ml side, and the glue on the coq side :
>
> Tactic Notation "apply'" constr_with_bindings(thm) tactic(c) :=
>  let name_of_case := fresh "NAMEOFCASE" in
>  (apply_aux thm resin name_of_case);
>  put_in_case name_of_case c.
>
> but when I try to use apply', it fails with :
> Error: This generic type is not supported in alias.
>
> My first question is: why not? I don't want to do anything clever with
> my "constr_with_bindings" from the coq side, I just want to pass it
> around. Shouldn't that be authorized ?
>
> The next question is : what can I do now ? :(
> My partial answer is : just write the glue directly on the caml side.
> But for that, I need to pass a not fully applied tactic as an
> argument, and I don't know how to do that.
>
> Is there a way for that? I guess it's the tactic[0-9] form, but it's
> rather obscure, and the only example I found that uses it
> (setoid_ring/newring.ml4) has a rather complicated way to apply the
> tactic. Is it the proper way to do that?
>
> Thanks for your help!
>
> Alexandre Pilkiewicz
>