Ssreflect Users Discussion List

[Ralf Jung <>]

Hi all,

I am having trouble with the following Notation after importing ssrfun:

Notation "{{ P }}" := (P) (at level 90).

(This is of course a reduced example, the notation I started with makes
more sense, but even this one fails).

After stepping over that notation in proof general, I cannot step back
to before it anymore. Instead, I get the following error message:

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

If I try stepping back a second time, the error changes to:

  Anomaly: Uncaught exception Not_found. Please report.

Also, if the definition occurs within a section, even running coqc on
the given file results in the same error.

Attached is a file demonstrating the issue.
If I remove the "Require Import ssrfun", everything works all right, as
expected.
Alternatively, if I reduce the "level" of the notation to 89, it also works.

I solved this in my Coq development by changing the level, but maybe
that's someone which could be fixed in SSReflect, or maybe I am doing
something wrong with the notation - it's certainly very surprising not
to be able tu step back suddenly.

Kind regards
Ralf

Require Import ssrfun.

Section TEST.

Notation "{{ P }}" := (P) (at level 90).

Goal {{ True }}.
Proof. tauto. Qed.

End TEST.