`Reset` не работает в CoqIDE

Question

Ни Reset <sectionname>., ни Reset <globalconstant>., ни Reset Initial. не работает в моих интерактивных сессиях CoqIDE. Сообщение

Error: Use CoqIDE navigation instead 

Единственные Reset s я видел в работе являются Reset Extraction Blacklist. и Reset Extraction Inline.. Ниже приведена копия некоторой информации из справки> О программе. Заранее спасибо за любые идеи

**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

Если вы хотите перейти на Coq 8.5, CoqIDE теперь поддерживает функции Reset, Undo, Abort, Restart ... Он просто распечатает предупреждение, в котором вам будет предложено использовать навигационные команды, когда вы их используете.

Answer 2

Из того, что я помню, Reset действие просто «идти в верхней части файла и забыть обо всем» стрелка, тот, который откатывается весь файл. Это сообщение здесь, чтобы предотвратить странное поведение путем смешивания таких команд с привязками IDE CoqIde

Редактировать после комментариев: В Coq нет реальной концепции «глобальных» переменных: это функциональный язык программирования. У вас есть доступ ко всему, что определено до вас. Он может быть в том же модуле или в импортированном модуле.

Если вы хотите избавиться от объявления верхнего уровня в том же модуле, единственный способ, которым я знаю, - переместить определение до той точки, в которой вы действительно нуждаетесь. Если он находится во внешнем модуле, который вы импортировали, единственное решение - не импортировать модуль.

Возможно, я ошибаюсь, пожалуйста, не стесняйтесь исправить меня. Я понимаю, что удаление такого определения заставляет вас удалять все, что зависит от этого определения, что не является простой задачей для выполнения.