Custom Query (361 matches)
Results (4 - 6 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #140 | fixed | PG takes a long time printing module types in Coq | ||
| Description |
Dear Proof General developers, I found a curious behavior: it seems that the time it takes PG to print the module type in Coq grows exponentially (or faster?) depending on the number of parameters in this module type. For example, I started with Module Type T. Parameter p1 : nat. End T. and started adding lines "Parameter p2 : nat.", "Parameter p3 : nat.", etc. Each time I issued the command Time Print Module Type T. after the closing of the module type T. Up to 4 parameters were printed practically instantaneously. When T had 5 parameters, the printing command took about 5 seconds, and when it had 6 parameters, it took about 60 seconds. In all cases the time requires by Coq as printed by the "Time" command was negligible (~ 0.001 s.). Also, I tried entering all these commands directly in coqtop, and again, printing was instantaneous. |
|||
| #152 | fixed | Faults with main regexps in XEmacs 21.5(b28) for Coq | ||
| Description |
The above version of XEmacs (standard XEmacs on Fedora 7) has problems with matching ends of commands properly. It trips up on the standard test |
|||
| #159 | wontfix | Goal centering | ||
| Description |
Is it possible to have the centering behavior of the *goals* window be configurable? I see from ticket #111 that the behavior was changed recently to center on the bottom of the goal instead of the top of the hypotheses, but unfortunately a lot of things I prove end up with 50 line goals, so the old behavior (while sometimes not ideal) is still better for me. |
|||
