diff options
Diffstat (limited to 'toplevel/ide_blob.ml')
| -rw-r--r-- | toplevel/ide_blob.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index c4b775912..8df17350c 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -173,9 +173,6 @@ let rec attribute_of_vernac_command = function | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand] | VernacExtend _ -> [] -let is_vernac_goal_starting_command com = - List.mem GoalStartingCommand (attribute_of_vernac_command com) - let is_vernac_navigation_command com = List.mem NavigationCommand (attribute_of_vernac_command com) |