Debugging code is now controlled by the debug flag.

[helm.git] / components / tactics / primitiveTactics.ml

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 16cff94d7796493f52a05658332a8261f564be4f..c9d68d9deccfe96770cf888097cfcc1797ec6a20 100644 (file)
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -335,8 +335,7 @@ let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
       (* TODO cacciare anche altre eccezioni? *)
   with 
   | CicUnification.UnificationFailure msg
-  | CicTypeChecker.TypeCheckerFailure msg ->
-      raise (Fail msg)
+  | CicTypeChecker.TypeCheckerFailure msg -> raise (Fail msg)
 
 (* ALB *)
 let apply_tac_verbose ~term status =