The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear Coq users and contributors,

can someone explain to me why in such case, apply tactic cannot determine
variable Q automatically (example is only "demo"):

Coq < Section Demo.

Coq < Axiom A : forall P Q : Prop, (P -> Q) -> P -> Q.
A is assumed

Coq < Parameter x y : nat.
x is assumed
y is assumed

Coq < Hypothesis H : x = 1 -> y = 2.
H is assumed

Coq <
Coq < Goal True.
1 subgoal

  H : x = 1 -> y = 2
  ============================
   True

Unnamed_thm <
Unnamed_thm < apply A in H.
Toplevel input, characters 1-13:
> apply A in H.
> ^^^^^^^^^^^^
Error: Unable to find an instance for the variable Q.

OK, "apply A with (Q := (y=2)) in H" help, but I don't want to know what
is value of Q. I want to do it automatically.

Thanks a lot,

-----------------------
Dr. Sc. Marko Malikoviæ
Filozofski fakultet
Sveuèili¹te u Rijeci
---------------------
Ph.D. Marko Malikoviæ
Faculty of Arts and Sciences
University of Rijeka, Croatia
-----------------------------