Custom Query (361 matches)
Results (31 - 33 of 361)
Ticket | Resolution | Summary | Owner | Reporter |
---|---|---|---|---|
#467 | fixed | The "Time (tactic)." vernacular command no longer displays timings unless the tactic finishes the proof | ||
Description |
It used to be the case (and still is the case in coqtop) that Goal True /\ True. split. Time idtac. Time constructor. Time constructor.
would display the timings of all three |
|||
#466 | fixed | parentheses in comments should not affect indentation level of non-comment code | ||
Description |
The second (** printing ¬( %\ensuremath{\neg}(% #¬(# *) Require Import Eqdep. Require Import Eqdep. Here's a workaround: (** printing ¬( %\ensuremath{\neg}(% #¬(# *) (* ))) *) Require Import Eqdep. Require Import Eqdep. |
|||
#463 | fixed | Warning messages suppress error messages and make PG have incorrect behavior with Coq | ||
Description |
The code
"compiles" in ProofGeneral with "Warning: This notation will not be used for printing as it is bound to a single variable", while it should fail with a type error. |
Note: See TracQuery
for help on using queries.