id,summary,reporter,owner,description,type,status,priority,milestone,component,resolution,keywords,cc
435,wrong behaviour of the period,coquser,David Aspinall,"I wonder if there is an issue with the treatment of the
colon? Below is my report (copied from the ssreflect mailing list):
A similar problem [see the quoted message below] occurred today with ssrcoq
trunk on my machine after updating to proofgeneral 4.2pre120112. Neither
executables of ssreflect nor the (trunk) libraries did change.
Calling from the command line by ""ssrcoq -compile"" succeeds as usual.
Only the emacs mode is broken.
The lemma
Lemma inord_rshift n (i : 'I_n) : inord i.+1 = rshift 1 i.
by rewrite rshift1 -lift0 inord_val. Qed.
now yields in proofgeneral:
Toplevel input, characters 34-41:
Error: In environment
n : nat
i : 'I_n
The term ""inord i"" has type ""'I_?19.+1"" which should be Set, Prop or Type.
The relevant lines in the *coq* buffer:
Coq < 18 || 0 < Lemma inord_rshift n (i : 'I_n) : inord i.+
Toplevel input, characters 34-41:
> Lemma inord_rshift n (i : 'I_n) : inord i.+
> ^^^^^^^
Error: In environment
n : nat
i : 'I_n
The term ""inord i"" has type ""'I_?9.+1"" which should be Set, Prop or Type.
Coq < 18 || 0 <
Regards,
Vladimir
On 25 January 2012 10:51, 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 ?
",defect,closed,major,PG-Emacs-4.2,2:pg-emacs,fixed,,