aboutsummaryrefslogtreecommitdiff
path: root/ide/coq_commands.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq_commands.ml')
-rw-r--r--ide/coq_commands.ml19
1 files changed, 3 insertions, 16 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 9598ee2f65..d51521ff71 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -194,14 +194,11 @@ let commands = [
let state_preserving = [
"Check";
"Eval";
- "Extract Constant";
- "Extract Inductive";
"Extraction";
- "Extraction Inline";
- "Extraction Language";
+ "Extraction Library";
"Extraction Module";
- "Extraction NoInline";
"Inspect";
+ "Locate";
"Print";
"Print All";
"Print Classes";
@@ -225,18 +222,13 @@ let state_preserving = [
"Pwd";
"Recursive Extraction";
- "Recursive Extraction Module";
+ "Recursive Extraction Library";
"Search";
"SearchAbout";
"SearchPattern";
"SearchRewrite";
- "Set Printing Coercion";
- "Set Printing Coercions";
- "Set Printing Synth";
- "Set Printing Wildcard";
-
"Show";
"Show Conjectures";
"Show Implicits";
@@ -252,9 +244,4 @@ let state_preserving = [
"Test Printing Wildcard";
"Recursive Extraction";
-
- "Unset Printing Coercion";
- "Unset Printing Coercions";
- "Unset Printing Synth";
- "Unset Printing Wildcard";
]