Opened 9 years ago

Closed 9 years ago

#435 closed defect (fixed)

wrong behaviour of the period

Reported by: coquser Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.2
Component: 2:pg-emacs Keywords:


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:

<prompt>Coq < 18
0 < </prompt>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.

<prompt>Coq < 18
0 < </prompt>

Regards, Vladimir

On 25 January 2012 10:51, Vincent Siles <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 ?

Change History (5)

comment:1 Changed 9 years ago by Erik Martin-Dorel


I experience the same issue with the current CVS version of ProofGeneral.

This seems to be a regression since PG 4.1 due to a change in the parsing of periods, as discussed in #296.

Kind regards,

Erik Martin-Dorel

comment:2 Changed 9 years ago by coquser

Summary: wrong behaviour of the colon?wrong behaviour of the period

Erik is right. I should have written about the period in the subject rather than about the colon. PG misunderstands the notation n.+1 that denotes (S n) in ssreflect. Same bug occurs in the release version 4.1.


comment:3 Changed 9 years ago by coquser

CORRECTION: the bug does not appear in 4.1 but only in 4.2. I had an unclear setup left from 4.2.


comment:4 Changed 9 years ago by courtieu

It should be fixed in cvs. Someone already confirmed but some more testing could be fine.

comment:5 Changed 9 years ago by courtieu

Resolution: fixed
Status: newclosed
Note: See TracTickets for help on using tickets.