Custom Query (361 matches)

Filters
 
Or
 
  
 
Columns

Show under each result:

Results (88 - 90 of 361)

← 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 →
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.

#468 wontfix Some notations with periods make PG hang David Aspinall coquser
Description 
Notation "a . 1" := (proj1_sig a) (at level 10).
Check (exist (fun x => x = x) 1 eq_refl) . 1.

Makes PG hang if I try to evaluate to after the 1.

#469 duplicate coqgeneral 4.3pre130327 does not compile with Emacs 24.3 David Aspinall coquser
Description

I have the following error at compile time:

generic/pg-response.el:104:23:Error: special-display-regexps' is an obsolete variable (as of 24.3); use display-buffer-alist' instead.

← 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 →
Note: See TracQuery for help on using queries.