better exception handling

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index fe7f176a0e5a3a8ed3a44e0d4c7e9a0228868da4..dab608e8ad0311e37c2c45456a257e8434cbabb0 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -13,7 +13,7 @@
 
 open Printf
 
-let debug = true
+let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 open Continuationals.Stack
@@ -22,7 +22,7 @@ module Ast = CicNotationPt
 
 let id_tac status = status ;;
 let print_tac print_status message status = 
-  if print_status then pp_tac_status status;
+  if print_status then pp_status status;
   prerr_endline message; 
   status
 ;;
@@ -244,7 +244,7 @@ let first_tac tacl status =
     (fun tac _ -> try Some (tac status) with NTacStatus.Error _ -> None) tacl
   in
     match res with
-      | None -> raise (NTacStatus.Error (lazy("No tactic left")))
+      | None -> fail (lazy "No tactics left")
       | Some x -> x
 ;;