Custom Query (361 matches)

Filters
 
Or
 
  
 
Columns

Show under each result:

Results (31 - 33 of 361)

← 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 →
Ticket Resolution Summary Owner Reporter
#467 fixed The "Time (tactic)." vernacular command no longer displays timings unless the tactic finishes the proof hendrik coquser
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 Time toplevel vernacular commands. In PG-emacs, only the final Time command gives me a timing in the response panel.

#466 fixed parentheses in comments should not affect indentation level of non-comment code David Aspinall coquser
Description

The second Require Import Eqdep. should not be indented so far. This is what happens when I highlight the four lines and press the TAB key. 

(** 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 David Aspinall coquser
Description

The code

Local Reserved Notation "'Ω'".

Record foo := {

A : Set where "'Ω'" := A; B : 1 = true

}.

"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.

← 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 →
Note: See TracQuery for help on using queries.