`Reset` funktioniert nicht in CoqIDE

Question

Weder Reset <sectionname>. noch Reset <globalconstant>. noch Reset Initial. funktioniert in meinen interaktiven CoqIDE-Sitzungen. Die Botschaft ist

Error: Use CoqIDE navigation instead 

Die einzigen Reset s ich an die Arbeit sind Reset Extraction Blacklist. und Reset Extraction Inline. gesehen habe. Unten finden Sie eine Kopie einiger Informationen aus Hilfe> Info. Vielen Dank im Voraus für alle Ideen

**Version information** 

The Coq Proof Assistant, version 8.4pl3 (January 2014) 
Architecture Linux running Unix operating system 
Gtk version is 2.24.23 
This is coqide.opt (opt is the best one for this architecture and OS) 

Answer 1

Wenn Sie ein Upgrade auf Coq 8.5 durchführen möchten, unterstützt CoqIDE jetzt Reset, Rückgängig, Abbrechen, Neu starten ... Es wird nur eine Warnung ausgegeben, die Sie stattdessen auf die Verwendung von Navigationsbefehlen hinweist.

Answer 2

Von dem, was ich mich erinnere, die Reset Aktion ist nur der „an die Spitze der Datei gehen und alles vergisst“ Pfeil, derjenige, der die gesamte Datei Backtracking. Diese Nachricht soll seltsames Verhalten verhindern, indem solche Befehle mit IDE-Bindings von CoqIde gemischt werden. Edit after comments: Es gibt kein wirkliches Konzept von "globalen" Variablen in Coq: es ist eine funktionale Programmiersprache. Sie haben Zugriff auf alles, was vor Ihnen definiert wurde. Es kann sich im selben Modul oder in einem importierten Modul befinden.

Wenn Sie eine Top-Level-Deklaration im selben Modul loswerden wollen, ist die einzige Möglichkeit, die ich kenne, die Definition bis zu dem Punkt zu verschieben, an dem sie wirklich benötigt wird. Wenn es sich um ein importiertes externes Modul handelt, besteht die einzige Lösung darin, das Modul nicht zu importieren.

Ich könnte falsch liegen, bitte zögern Sie nicht, mich zu korrigieren. Mein Verständnis ist, dass das Entfernen einer solchen Definition Sie zwingt, alles zu entfernen, was von dieser Definition abhängt, was keine einfache Aufgabe ist.