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

2 files changed, 1 insertions, 12 deletions

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
+