CoqIDEでリセットが動作しない

Reset <sectionname>.でもReset <globalconstant>.でもReset Initial.もCoqIDEインタラクティブセッションで動作しません。メッセージは、私が仕事に見てきた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)

出典

2016-03-26 jaam

Coq 8.5にアップグレードする場合、CoqIDEはリセット、元に戻し、中止、再起動をサポートするようになりました。ナビゲーションコマンドを使用するときに代わりにナビゲーションコマンドを使用するよう警告する警告が表示されます。

出典

2016-04-21 11:43:10

ありがとうございました。 https://coq.inria.fr/coq-85）にはLinuxインストーラがないので、O'Camlをインストールしてソースなどをコンパイルする必要があります。 – jaam

Coq開発者はOpam経由でインストールすることをお勧めします（ただし、 'liblablgtk2-ocaml-dev'パッケージが最初にインストールされていることを確認する必要があります）。もう一つの標準ではないがより迅速な解決策は、[Nix]（http://nixos.org/nix/）のようないくつかの代替パッケージマネージャでインストールすることです。一言で言えば、 'curl https://nixos.org/nix/install | sh'それから 'nix-env -i coq-8.5pl1' –

ための事前のおかげで、Reset行動であるだけで「ファイルの先頭に移動し、すべてを忘れて」矢印、ファイル全体をバックトラック1。このメッセージは、CoqIdeのIDEバインディングとそのようなコマンドを混ぜ合わせることによって奇妙な動作を防ぐためのものです。

コメントの後に編集： Coqの "グローバル"変数の実際の概念はありません。あなたはあなたより前に定義されたものにアクセスできます。これは、同じモジュール内またはインポートされたモジュール内にあることができます。

同じモジュールで最上位レベルの宣言を取り除きたい場合、私が知っている唯一の方法は、必要なポイントまで定義を下に移動することです。インポートした外部モジュールにある場合、唯一の解決策はモジュールをインポートすることではありません。

私は間違っている可能性があります、私を修正することを躊躇しないでください。私の理解では、このような定義を削除すると、この定義に依存するものを削除することが強制されます。これは実行する簡単なタスクではありません。

出典

2016-03-29 06:56:50 Vinz

OK、グローバル変数をコード内で却下するにはどうしたらいいですか？私はそれが 'Reset Initial.'と' Reset .'が – jaam

のものだと思ったのですが、 "dismiss"とはどういう意味ですか？ – Vinz

"clear"、 "reset" .. – jaam

CoqIDEでリセットが動作しない

答えて

関連する問題