summaryrefslogtreecommitdiff
path: root/vernac/vernacprop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacprop.ml')
-rw-r--r--vernac/vernacprop.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index a837b77a..0fdd2faa 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -31,7 +31,6 @@ let rec has_Fail = function
let is_navigation_vernac_expr = function
| VernacResetInitial
| VernacResetName _
- | VernacBacktrack _
| VernacBackTo _
| VernacBack _ -> true
| _ -> false