Ssreflect Users Discussion List

[Jason Gross <>]

Hi,

Here is some code that gives the anomaly.  Replacing "first foo" with "[ foo | .. ]" makes it go away, which makes me think this is an ssr bug.

Ltac foo :=  

  idtac;

  try (idtac;

       let e := fresh "e" in

       match False with

         | True => idtac

       end;

       first foo).

Goal True.

  foo.

I'm using ssr 1.4, Coq 8.4pl4.

-Jason