The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hi everybody,
I want to define a tactic that has an argument H which is a name of an 
hypothesis of the context that  will be used if some conditions are 
verified to simplify the current goal
An example of such tactics is the following one: elimAnd

Ltac elimAnd H:=
match goal with H:?A/\?B |- _=>elim H; clear H; intros
| _ =>idtac
end.

The tactic that I want to define has one argument H , the tactic has to 
check that the type of H is of the form A/\B if this is the case the 
tactic elim this hypothesis otherwise it does nothing
Unfortunately while trying to test elimAnd I found that it doesn't 
always elim the hypothesis whose name is given as a parameter specially 
when the context contains several hypothesis of the form _/\_!

An example of that is the following:
Lemma tryTac:forall (A B:Prop), A/\B ->A/\A->B.
intros A B H H0.
elimAnd H.
-------here the tactic elim H0 instead of H!!

How can we solve the probleme without defining the tactic in ocaml?

Concerning the definition of tactics using ocaml is there any tutorial 
explaining that and giving some basic examples??
Thanks a lot in advance

Houda

--
==============================
|      Houda ANOUN           |
|         LaBRI              |
| 351 Cours de la libération |
|      33405 Talence         |
|    phone: 0540002489       |
|  e-mail 
:anoun AT labri.fr
    |
=============================