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)
Change History (3)
Changed 20 years ago by reilles@…
comment:1 Changed 20 years ago by gwright@…
| Status: | new → assigned |
|---|
I'm building now (w/ the current ocaml).
/gw
comment:2 Changed 20 years ago by gwright@…
| Resolution: | → fixed |
|---|---|
| Status: | assigned → closed |
Committed. Thanks!
Note: See
TracTickets for help on using
tickets.
the patch