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,,