Ssreflect Users Discussion List

[Assia Mahboubi <>]

Bas Spitters a écrit :
> A few days ago we tried to compile ssr with coq trunk, but got an error:
> Unbound constructor PrimaryTable
>
> Is anyone maintaining a version of ssr compatible with Coq trunk or should we 
> wait for the stable release?
>
> Bas
>   
Thanks to the port of François Garillot and to the maintenance work of 
Coq developers, the directory :
http://gforge.inria.fr/projects/coq-contribs/Saclay/Ssreflect
now contains a version of ssreflect which complies with todays's Coq 
trunk version. In particular the src/ subdirectory contains the .ml file 
for the extendend top-level. The theories/ subdirectory contains many .v 
files mainly there for benchmarking reasons.
Note that the status of this contrib is somehow experimental:
- it contains a version of the 1.2 release source files which is ported 
day by day by Coq developers (and sometimes us) to comply with the ever 
changing Coq trunk.
- the compilation may be broken by any change in Coq trunk, and 
sometimes the contribution remains broken for several days.
- the next release of ssreflect could differ a lot from this code, both 
with respect to .ml and .v files, to introduce new features and/or 
optimizations.

Hope this helps,

assia