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