4 files changed, 16 insertions, 16 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index e960170354..7b62ef1660 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -392,3 +392,12 @@ let make_cases s =
 	  tarr
 	  []
     | _ -> raise Not_found
+
+let is_state_preserving = function
+  | VernacPrint _ | VernacPrintOption _ | VernacGlobalCheck _
+  | VernacCheckMayEval _ | VernacSearch _ | VernacLocate _ 
+  | VernacShow _ | VernacMemOption _ | VernacComments _ 
+  | VernacChdir None | VernacNop -> 
+      prerr_endline "state preserving command found"; true
+  | _ -> 
+      false
diff --git a/ide/coq.mli b/ide/coq.mli
index 3acc686834..8625e93eeb 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -20,6 +20,7 @@ val interp : string -> Util.loc * Vernacexpr.vernac_expr
 val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
 
 val is_tactic : Vernacexpr.vernac_expr -> bool
+val is_state_preserving : Vernacexpr.vernac_expr -> bool
 
 (* type hyp = (identifier * constr option * constr) * string *)
 
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";
 ]
diff --git a/ide/coqide.ml b/ide/coqide.ml
index ae7dfbec57..26bb80b05f 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1236,6 +1236,9 @@ Please restart and report NOW.";
 		   raise e
 		 end);
 	      update_input ()
+	  | { ast = (_, a) } when is_state_preserving a ->
+	      ignore (pop ());
+	      update_input ()
 	  | _ -> 
 	      self#backtrack_to_no_lock start
 	  end;