Ssreflect Users Discussion List

[Enrico Tassi <>]

On Tue, Dec 18, 2012 at 07:10:15PM +0100, Jose Grimm wrote:
> coq8-4/user-contrib/Ssreflect, and was created three months ago.
> 
> How do I recreate this file ? should I execute make in the directory
> ssreflect/ssreflect1.3_v8.4, followed by make install ? Ids is the
> necessary to  recomplies all files in the trunk ?

The content of ssreflect/ssreflect1.3_v8.4 is indeed what was released
as ssreflect 1.4 (the directory name is misleading, it will be
eventually renamed). Do as you did to compile and install ssreflect.

Assuming you have COQBIN properly set, typing make && make install inside
ssreflect/ssreflect1.3_v8.4 should do the job. Of course this will
compile the libraries in ssreflect/ssreflect1.3_v8.4/theories/ too (that
are the ones release with ssr 1.4.

But I guess you are using the ones in trunk/.
To avoid recompiling libraries you don't need, you can (untested):

  export COQBIN=...
  cd ssreflect/ssreflect1.3_v8.4/
  make Makefile.coq
  make -f Makefile.coq theories/ssreflect.cmxs
  cp theories/ssreflect.cmxs .../user-contrib/Ssreflect/

Cheers
-- 
Enrico Tassi