Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

Hello,

I have just noticed that I get an error when I do

================8<================
$ rlwrap ~/src/coq-8.4/bin/coqtop

Coq < Require Import ssreflect fintype ssrnat.
Small Scale Reflection version 1.4 loaded.
...

Coq < Reset Initial.
No level labelled "3" in entry "constr:pattern"
Anomaly: Uncaught exception Failure("Grammar.extend"). Please report.

Coq < Reset Initial.
Anomaly: uncaught exception Not_found. Please report.
================8<================

I also get this error when calling (proof-retract-buffer) in ProofGeneral
on a file where [ssrnat] is not properly loaded before [fintype].

Is it normal?

Kind regards,

Erik

-- 
Érik Martin-Dorel
Post-doctorant, Équipe-projet Marelle
Inria Sophia Antipolis - Méditerranée
http://erik.martin-dorel.org/