aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacprop.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacprop.mli')
-rw-r--r--vernac/vernacprop.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli
index eb7c7055a..df739f96a 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
+