Custom Query (361 matches)

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.

Hi,

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

Bye,

Hendrik

[reported by Hendrik Tews on PG-devel list]

when you kill the currently active scripting buffer, then the hooks in proof-deactivate-scripting-hook are not run when the buffer was fully asserted. I believe this is a bug.

What happens is that

- kill-buffer-hook calls proof-script-kill-buffer-fn,
- which calls proof-deactivate-scripting-auto
- which calls (proof-deactivate-scripting 'process)
- which calls (proof-protected-process-or-retract 'process)
- which calls proof-process-buffer
- which calls (proof-assert-until-point-interactive)
- which calls proof-assert-until-point
- which throws 
     (error
	 "At end of the locked region, nothing to do to!"))
- this error unwinds until the ignore-errors in
 proof-deactivate-scripting-auto, thereby skipping the call to
 the hooks in proof-deactivate-scripting