Ssreflect Users Discussion List

[Georges Gonthier <>]

  Indeed, you are right. I'm guessing that Coq traverses exported Ltac 
scripts at module load time in order to substitute functor arguments, even 
when there are no functors involved. This means that theorems proved in a 
file that uses Ltac tactics which use a plugin, can only be used if the 
plugin is present. In the ssreflect library, we could work around this issue 
by rewriting the handful of Ltac tactics in primitive Coq, but this will 
probably be inconvenient for other users. Ideally, a plugin shouldn't be 
required by a client of a library until it either
  a) Runs an Ltac definition that uses some plugin tactic or tactic argument 
extension
  b) Imports a submodule that exports a new kind of object defined in the 
plugin
  c) Requires a submodule that contains a new kind of global object
Note that ssreflect does neither b) nor c), which could be harder to achieve 
with the current implementation of modules.

Georges

-----Original Message-----
From: Stéphane Glondu [] 
Sent: 08 September 2009 15:27
To: Georges Gonthier
Cc: Guillaume Melquiond; ; Hugo Herbelin
Subject: Re: Ssreflect and corn

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