The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

 I don't know what is the expected result from apply in this case, but
you can always perform a rewrite in the goal or in the hypothesis:

  rewrite <- Qlt_alt.

or

  rewrite Qlt_alt in H.


On Thu, May 9, 2013 at 10:32 AM, Daniel de Rauglaudre
<daniel.de_rauglaudre AT inria.fr>
 wrote:
> 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/