Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hi again Reynald,

> I have a small ssr development that relies on polydiv.v that is not
> distributed with ssreflect-1.3pl1 (I used Coq trunk just for 
> ssreflect1.3_trunk).

But then you should not need Coq trunk to compile it, but the dev version of
ssreflect, which is stored in:

coqfinitgroup/trunk/ssreflect/ssreflect1.3_v8.3

and which is to be built with the standard distribution of coq 8.3pl1.

The directory:

coqfinitgroup/trunk/ssreflect/ssreflect1.3_v8.3/theories

contains the same .v files as the distributed version, so you will only be
interested in compiling the .ml plugin. Once compiled the static executable or
the dynamic plugin, you will be able to compile any library under

coqfinitgroup/trunk/


Do not hesitate to let us know about any problem you may encounter.

Note however that I am right now performing heavy changes in the polydiv.v 
file,
mainly to provide exact Euclidean division for polynomials when coefficients 
are
equipped with a field structure.

A nasty consequence might be that you will have to update your development 
once
I commit it into the repository... Do not hesitate to send me your development
by private email so that I can help you to port it and so that it helps me
improving my documentation.

Hope this helps,

assia