Custom Query (361 matches)
Results (115 - 117 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #369 | fixed | PG will not compile under non-windowing Emacs | ||
| Description |
emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_ports_math_ProofGeneral/work/ProofGeneral-4.0pre101004/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego pgshell phox generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile generic/pg-pbrpm.el In toplevel form: generic/pg-pbrpm.el:599:1:Error: the following functions are not known to be defined: popup-menu, mouse-set-point make[1]: * [generic/pg-pbrpm.elc] Error 1 make: * [compile] Error 2 |
|||
| #368 | needmoreinfo | coq, already defined values | ||
| Description |
Hi, The following code is rejected by Coq, since [x] is already defined in the second line, but proofgeneral "validates" it (it goes through, so that one has to be really careful to notice the warning in the "coq output" buffer - this can be quite errorprone since Coq keeps the old definition). << Definition x := 3. Definition x := 5. Damien |
|||
| #366 | fixed | Fix documentation for mouse button commands | ||
| Description |
The manual has an incomplete list and bindings which are old. |
|||
