Ssreflect Users Discussion List

[Enrico Tassi <>]

On Mon, Aug 05, 2013 at 07:26:54PM +0200, Erik Martin-Dorel wrote:
> I have four minor remarks related to the release candidates:

Thanks for testing the rc!

> 1) With ssreflect-1.5rc1.tar.gz: $(make clean) raises an error
> 3) As regards "mathcomp-1.5rc1.tar.gz", would it be worth it to use
> the same wrapper as ssreflect-1.5/Makefile for adding a trailing slash

you are certanly right here

> 2) I also tested the static compilation, and once the plug-in has been
> compiled with Coq 8.4pl2, I get the error
> >bin/ssrcoq -q  -I src -R theories Ssreflect   -compile theories/ssrmatching
> >Error: cannot guess a path for Coq libraries; please use -coqlib option

Can you confirm you configure coq with the -local flag?

> 4) Finally I would like to propose a workaround related to the
> pretty-printing of some MathComp notations: if we issue for example
> What is your opinon on this change?

I'll let the notation experts comment this issue.

Cheers and thanks again for testing
-- 
Enrico Tassi