Ssreflect Users Discussion List

[Jason Gross <>]

The bug tracker doesn't like me at the moment, but here's a smaller test case:

$ cat bar.v

Reserved Notation "f1 =1 f2 :> A" (at level 70, f2 at next level, A at level 90).

$ cat foo.v

Require Coq.Unicode.Utf8_core.

Require bar.

Import bar.

Import Coq.Unicode.Utf8_core.

Back 2.

$ ~/.local64/coq/coq-8.4pl4/bin/coqc bar.v && ~/.local64/coq/coq-8.4pl4/bin/coqtop < foo.v

Welcome to Coq 8.4pl4 (August 2014)

Coq <

Coq <

Coq <

Coq <

Coq < No level labelled "91" in entry "constr:pattern"

Anomaly: Uncaught exception Failure("Grammar.extend"). Please report.

Coq <

On Wed, Oct 22, 2014 at 5:46 PM, John Wiegley <> wrote:

>>>>> 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