The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hello,

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?

Thanks.

--
gregory malecha