The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi,

I don't know if it is a bug or something I don't know, but I have a
problem with 'apply' when the applied theorem is a iff:

Example:

  Require Import QArith.
  Example foo : ∀ x y, x < y → (x ?= y) = Lt.
  Proof.
  intros.
  apply Qlt_alt.
--> nothing happens !
  apply Qlt_alt in H.
--> nothing happens !

Is there a way to tell 'apply' to apply Qlt_alt the direction I want?
Why was there no error message and nothing happened?

Tested on 8.4 and trunk.

Thanks.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/