Custom Query (361 matches)

Filters
 
Or
 
  
 
Columns

Show under each result:

Results (85 - 87 of 361)

← 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 →
Ticket Resolution Summary Owner Reporter
#461 fixed old manuals on website David Aspinall coquser
Description

Hi,

the PG website still shows the 4.1 version of both manuals (both html and pdf).

Bye,

Hendrik

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

#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.
← 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 →
Note: See TracQuery for help on using queries.