Ssreflect Users Discussion List

[John Wiegley <>]

>>>>> John Wiegley <> writes:

> I'm going to try tracking it down a little better today, but it interferes
> with smooth Proof General usage quite a bit.

I wasn't able to get it any smaller, but this simple script will demonstrate
the problem:

  bug.v:
    Require Import Ssreflect.ssrfun.
    Require Import Coq.Unicode.Utf8_core.
    BackTo 1.

John