The Coq mailing list

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

Dear list.

I am working on some tactics, and I would like to have them behaves
"like destruct" in the following sens:

destruct accepts either an ident of a constr. If it's an ident, and it
is not introduced yet, it performs an "intros until".

The only way I found to simulate this is:


Tactic Notation "exists_hyp" hyp(H) :=
  idtac.

Tactic Notation "ointros" ident(id) :=
  first [exists_hyp id | intros until id|idtac].

Tactic Notation "mydestruct" constr(trm) :=
  do_something trm.

Tactic Notation "mydestruct" ident(trm) :=
  ointros trm;
  do_something trm.


But this forces me to duplicate all my code, and I have several
versions of mydestruct, some with "as" patterns for example (on a side
note, I sadly can't find a way to use as_ipat or with_induction_names,
so I have to deal with each case separately.)

So what I'm looking for is some sort of constr_or_ident, or even
"any". Does that exists ? Then I would be able to write something like

Tactic Notation "exists_hyp" hyp(H) :=
  idtac.

Tactic Notation "ointros" any(id) :=
  first [exists_hyp id | intros until id|idtac].

Tactic Notation "mydestruct" any(trm) :=
  ointros trm;
  do_something trm.


Thanks in advance

Alexandre