Opened 14 years ago
Closed 13 years ago
#363 closed defect (fixed)
Multiple file handling for Coq needs sensible treatment
| Reported by: | David Aspinall | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.1 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: |
Description
We need to find a way to make Proof General development across multiple files mesh smoothly with Coq users' main Makefile-based batch build mechanism. In particular, undoing across completed scripts should behave consistently and work with Coq's top level.
Change History (3)
comment:1 Changed 14 years ago by
| Milestone: | PG-Emacs-4.0 → PG-Emacs-4.1 |
|---|---|
| Status: | new → accepted |
comment:2 Changed 13 years ago by
Work in progress by Hendrik Tews on this, see http://askra.de/software/multiple-coq/ for experimental patch.
comment:3 Changed 13 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | accepted → closed |
Hendrik's patch is now incorporated. Works nicely!
Note: See
TracTickets for help on using
tickets.
Postponing this improvement for this release.
Have discussed this with Pierre and he considers it something that is not a priority (Coq users should understand the way things work and figure it out). But it would be nice to document the recommended ways of working, perhaps, to help new users.
There is some old email to mine discussing various possible clean solutions.