Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Jul 12, 2017 at 06:08:15PM +0200, Yves Bertot wrote:
> Here is my analysis of the situation.
> 
> I believe that compiling the current head of the master branch of math-comp
> with coq-8.6 cannot work because the whole content of ssreflect.v has been
> removed (under the assumption that the content of this file is now part of
> the coq distribution, something that only is true in the current master
> development branch of Coq and will be true in the next released version).

The way the build system works is that, once the coq version has been
detected, all missing piece of data are put in place.  In
ssreflect/plugin/$VERSION/ you can find what is missing in
Coq $VERSION in order to compile the thing.  e.g. .../trunk/ is empty,
.../8.6/ contains the ssreflect.ml4 + the few .v that were merged in,
.../8.5/ contains ssreflect.ml4, ssrmatching.ml4, and the .v files.

The Makefile in ssreflect/Makefile.coq-makefile is in charge of putting
back what is missing.  So detecting the right version of Coq is crucial.

Note that the makefile uses $COQBIN/coqtop to find out which version of
coq you are using (if COQBIN is set) or the coqtop in the PATH.

Hope it helps.

Ciao
-- 
Enrico Tassi