OCaml and Coq tactics
I'm new on this list and didn't learn OCaml yet. The reason why I'm here is that one Coq tactic is missing for my needs.
So, my questions are:
1. Somebody use Coq on this list?
2. Do you think I can write new tactic in Objective Caml which will allow me to compare hypotheses with the same ident over different subgoals and will allow me to do "something" if all hypotheses have equal values and "something else" if all hypotheses haven't equal values? So, can I surmount a independents of subgoals? I don't like to spend a time to learn OCaml for nothing:)
H : x=value_1
H : x=value_2
H : x=value_n
So, I need tactic (or tactical) which will apply one tactic if value_1, value_2,..., value_n are equal in all subgoals, but will apply another tactic if value_1, value_2,..., value_n are not equal.
Thanks you very much for your help or for your opinion,
Greetins from Croatia,
You rock. That's why Blockbuster's offering you one month of Blockbuster Total Access, No Cost.
[Non-text portions of this message have been removed]
- Coq has a mailing list and I think you'll get much better answers by
posting your question there: