The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> I'm trying to write a tactic that will convert equivalences on N to
> equivalences on nat, but I'm having a problem applying nat_compare_lt to a
> hypothesis that I find using a match. I've boiled it down to this simple
> example:
> 
> Require Import Compare_dec.
> Goal forall a b, nat_compare a b = Lt -> True.
>   intros.
>   (** If I do: **)
>   apply <- nat_compare_lt in H. (** it succeeds **)
> 
>   (** If I do: **)
>   match goal with 
>     | [ H : _ |- _ ] => idtac H;
>       apply <- nat_compare_lt in H
>   end. (** it fails but it prints H as one of the hypotheses tried **)
> 
> Is this a bug? Does anyone know of a way to work around this?

Yes, this is a bug. You can either retrieve and compile the svn 8.3 or
trunk version, or simply temporarily overwrite the "apply <- ... in ..." 
and "apply -> ... in ..." tactic notations by adding the following
lines to your file:

  Tactic Notation "apply" "->" constr(lemma) "in" hyp(J) :=
  bapply lemma ltac:(fun H => destruct H as [H _]; apply H in J). 

  Tactic Notation "apply" "<-" constr(lemma) "in" hyp(J) :=
  bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J). 

Best regards,

Hugo Herbelin