Ssreflect Users Discussion List

[Mathieu Boespflug <>]

Hrm.... as always, forgot the attachment.

-- Mathieu


On Thu, Feb 9, 2012 at 7:56 PM, Mathieu Boespflug
<> wrote:
> 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
Activated option "Automatic Coercions Import" so that ReleasedSsreflect
compile after Coq v8.3 revision 14776 fixed unexpected import of
coercions in innermost modules of a chain of nested module when
only outermost module is imported.

--- ssreflect-1.3pl2-old/theories/ssreflect.v	2011-03-25 05:12:49.000000000 -0400
+++ ssreflect-1.3pl2/theories/ssreflect.v	2012-02-09 18:05:35.005771434 -0500
@@ -3,6 +3,7 @@
 Require Import Bool. (* For bool_scope delimiter 'bool'. *)
 
 Declare ML Module "ssreflect".
+Global Set Automatic Coercions Import.
 
 (***************************************************************************)
 (* This file is the Gallina part of the ssreflect plugin implementation.   *)