aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq_commands.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq_commands.ml')
-rw-r--r--ide/coq_commands.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 61f8afaef..a2db621fd 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -240,6 +240,8 @@ let state_preserving = [
"Test Printing Let";
"Test Printing Synth";
"Test Printing Wildcard";
+
+ "Recursive Extraction";
"Unset Printing Coercion";
"Unset Printing Coercions";