dead code pruning

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

1 files changed, 0 insertions, 25 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 505140cf26..2efbe20d38 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -459,36 +459,11 @@ let interp_and_replace s =
   let msg = read_stdout () in
   result,msg
 
-let nb_subgoals pf =
-  List.length (fst (Refiner.frontier (Tacmach.proof_of_pftreestate pf)))
-
 type tried_tactic = 
   | Interrupted
   | Success of int (* nb of goals after *)
   | Failed
 
-let try_interptac s = 
-  try
-    prerr_endline ("Starting try_interptac: "^s);
-    let pf = get_pftreestate () in
-    let pe = Pcoq.Gram.Entry.parse 
-	       Pcoq.main_entry 
-	       (Pcoq.Gram.parsable (Stream.of_string s)) 
-    in match pe with 
-    | Some (loc,(VernacSolve (n, tac, _))) ->
-	let tac = Tacinterp.interp tac in
-	let pf' = solve_nth_pftreestate n tac pf in
-	prerr_endline "Success";
-	let nb_goals = nb_subgoals pf' - nb_subgoals pf in
-	Success nb_goals
-    | _ ->
-	prerr_endline "try_interptac: not a tactic"; Failed
-  with 
-  | Sys.Break | Stdpp.Exc_located (_,Sys.Break)
-      -> prerr_endline "try_interp: interrupted"; Interrupted
-  | Stdpp.Exc_located (_,e) -> prerr_endline ("try_interp: failed ("^(Printexc.to_string e)); Failed
-  | e -> Failed	  
-
 let rec is_pervasive_exn = function
   | Out_of_memory | Stack_overflow | Sys.Break -> true
   | Error_in_file (_,_,e) -> is_pervasive_exn e