diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2003-02-20 17:37:33 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2003-02-20 17:37:33 +0000 |
| commit | 06e57f092923313915e128032c11738068ff8db2 (patch) | |
| tree | faad346b00f844e0c41c84694631ad1d803973f6 /html/devel.html | |
| parent | 7332d691f879ddaa23426baafee1b019ed099715 (diff) | |
corrected a bug of pg/coq, the following line was not recognized as a
module start:
Module M:T with Definition A:=u.
I had to count the number of 'with' and ':=' to know if the last ':='
was a Module given explicitely (--> no module start) or only part of a
'with ...:=' (--> module start).
Diffstat (limited to 'html/devel.html')
0 files changed, 0 insertions, 0 deletions