Ssreflect Users Discussion List

[Mathieu Boespflug <>]

Hi Vincent,

I was having the same problem but the attached patch fixed the problem
for me.

Now, if only I figure out why make doesn't produce an ssrcoq
executable...

All the best,

-- Mathieu


On Wed, Jan 25, 2012 at 11:51:35AM +0100, Vincent Siles wrote:
> Hi there, since lots of stuff have changed in coq-svn v8.3 recently, I
> decided to upgrade it this morning and recompile ssr, but
> I have the following error (dynamic plugin compilation):
> 
> /home/vinz/boulot/coq/v8.3/bin/coqc  -q  -R theories Ssreflect -R src
> Ssreflect   theories/fintype
> File 
> "/home/vinz/boulot/coq/ssreflect-svn/trunk/ssreflect/ssreflect1.3_v8.3/theories/fintype.v",
> line 131, characters 44-45:
> Error: In environment
> T : eqType
> e : seq ?15
> The term "T" has type "eqType" while it is expected to have type
>  "pred_sort ?21".
> make: *** [theories/fintype.vo] Erreur 1
> 
> I'm using the svn version of Coq 8.3
> 
> [vinz@hauru ssreflect1.3_v8.3]$ $COQBIN/coqtop.byte -v
> The Coq Proof Assistant, version 8.3pl3 (January 2012)
> compiled on janv. 25 2012 11:17:29 with OCaml 3.12.1
> 
> svn info gives:
> 
> Révision : 3533
> Révision de la dernière modification : 3466
> Date de la dernière modification: 2011-11-21 15:14:22 +0100 (lun. 21 nov. 
> 2011)
> 
> 
> Do I have to backtrack to pl2 ? My goal is to use Coq 8.3 and the
> librairies of ssr 1.3
> (I don't want to use the thoeries of the trunk since I want other
> people to be able to compile
> my files).
> 
> Any suggestions ?
> 
> Best,
> Vincent