The Coq mailing list

[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