remove some unused functions (which are part of a soon-to-be obsolete

framework anyway)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12199 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 14 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index fbb8759d1..5572dd8ae 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -324,9 +324,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)
 
@@ -344,17 +341,6 @@ let is_vernac_goal_printing_command com =
   List.mem GoalStartingCommand attribute or
   List.mem SolveCommand attribute
 
-let is_vernac_state_preserving_command com =
-  let attribute = attribute_of_vernac_command com in
-  List.mem OtherStatePreservingCommand attribute or
-  List.mem QueryCommand attribute
-
-let is_vernac_tactic_command com =
-  List.mem SolveCommand (attribute_of_vernac_command com)
-
-let is_vernac_proof_ending_command com =
-  List.mem ProofEndingCommand (attribute_of_vernac_command com)
-
 type undo_info = identifier list * int
 
 let undo_info () = Pfedit.get_all_proof_names (), Pfedit.current_proof_depth()