aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq_commands.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-04-16 22:26:57 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-04-16 22:26:57 +0000
commitd48565c932c0f540af5a4a435123499ba86b4882 (patch)
tree2a073310629162192cd87c54977f5e55edcdbc04 /ide/coq_commands.ml
parent8568214f1b7950fe9c5d95c04e851c00f49751ce (diff)
oubli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3932 85f007b7-540e-0410-9357-904b9bb8a0f7
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";