Merge PR #6492: Remove query-in-IDE warning.

3 files changed, 2 insertions, 15 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index aafc3fc59a..5f40a22423 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -69,9 +69,7 @@ let ide_cmd_checks ~id (loc,ast) =
   if is_known_option ast then
     warn "Set this option from the IDE menu instead";
   if is_navigation_vernac ast || is_undo ast then
-    warn "Use IDE navigation instead";
-  if is_query ast then
-    warn "Query commands should not be inserted in scripts"
+    warn "Use IDE navigation instead"
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index bd2d0261ad..4fdc78dd2a 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -53,17 +53,6 @@ let is_debug cmd = match under_control cmd with
   | VernacSetOption (["Ltac";"Debug"], _) -> true
   | _ -> false
 
-let is_query cmd = match under_control cmd with
-  | VernacChdir None
-  | VernacMemOption _
-  | VernacPrintOption _
-  | VernacCheckMayEval _
-  | VernacGlobalCheck _
-  | VernacPrint _
-  | VernacSearch _
-  | VernacLocate _ -> true
-  | _ -> false
-
 let is_undo cmd = match under_control cmd with
   | VernacUndo _ | VernacUndoTo _ -> true
   | _ -> false
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli
index eb7c7055ac..df739f96a9 100644
--- a/vernac/vernacprop.mli
+++ b/vernac/vernacprop.mli
@@ -21,6 +21,6 @@ val has_Fail : vernac_control -> bool
 val is_navigation_vernac : vernac_control -> bool
 val is_deep_navigation_vernac : vernac_control -> bool
 val is_reset : vernac_control -> bool
-val is_query : vernac_control -> bool
 val is_debug : vernac_control -> bool
 val is_undo : vernac_control -> bool
+