Opened 20 years ago

Closed 20 years ago

#2672 closed defect (fixed)

UPDATE: coq-8.0pl2

Reported by: reilles@… Owned by: macports-tickets@…
Priority: Normal Milestone:
Component: ports Version: 1.0
Keywords: Cc:
Port:

Description

Mainly bug fixes.

Changes from V8.0 patch level 1 to V8.0 patch level 2

Notations: Option "format" now aware of recursive notations

Bug fixes:

  • Tactic "fail n" for n<>0 now works (notice that each "match term with" block decreases the failure

level, in accordance with the intuition but not in conformity with the reference manual)

  • Option -dump-glob now strips module segment as expected by coqdoc (which is still not aware of

modules)

  • See coq-bugs web page for a full list of fixed bugs (look for fixes committed before Jan 2005 to cvs

version V8-0-bugfix)

Attachments (1)

coq.diff (2.4 KB) - added by reilles@… 20 years ago.
the patch

Download all attachments as: .zip

Change History (3)

Changed 20 years ago by reilles@…

Attachment: coq.diff added

the patch

comment:1 Changed 20 years ago by gwright@…

Status: newassigned

I'm building now (w/ the current ocaml).

/gw

comment:2 Changed 20 years ago by gwright@…

Resolution: fixed
Status: assignedclosed

Committed. Thanks!

Note: See TracTickets for help on using tickets.