Ssreflect Users Discussion List

[Stéphane Glondu <>]

Guillaume Melquiond a écrit :
> Note that there is a major downside though: it makes it impossible to 
> import an SSReflect-compiled file from a standard Coq proof.

Is that even possible?

Georges Gonthier a écrit :
> You can therefore load an ssreflect .vo file within "Coq classic" and 
> almost everything will work [...]

---8<--------------------------------------------------------------
glondu@aspirine:~/ssreflect/theories$ coqtop -I ../src
Welcome to Coq 8.2pl1 (July 2009)

Coq < Require Import ssreflect.
Anomaly: uncaught exception Failure "No interpretation function found
for entry ssrdoarg".
Please report.

Coq < Declare ML Module "ssreflect".
[Loading ML file ssreflect.cmxs ... done]

Coq < Require Import ssreflect.

Coq <
---8<--------------------------------------------------------------

It looks like the extension must always be "there" to use ssreflect's
libraries. Or am I missing something?


Cheers,

-- 
Stéphane