Opened 12 years ago
Closed 12 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: | |
Cc: |
Description
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:
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.
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 12 years ago by
comment:2 Changed 12 years ago by
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.
--Vladimir
comment:3 Changed 12 years ago by
CORRECTION: the bug does not appear in 4.1 but only in 4.2. I had an unclear setup left from 4.2.
--Vladimir
comment:4 Changed 12 years ago by
It should be fixed in cvs. Someone already confirmed but some more testing could be fine.
comment:5 Changed 12 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Hello,
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