From f871bbfd9a39012ff5a9b227b535ee2d3765615b Mon Sep 17 00:00:00 2001
From: vgross
Date: Mon, 22 Jun 2009 09:31:45 +0000
Subject: 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
---
 ide/coq.ml | 14 --------------
 1 file changed, 14 deletions(-)

diff --git a/ide/coq.ml b/ide/coq.ml
index fbb8759d1b..5572dd8aee 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()
-- 
cgit v1.2.3