]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/tacticals.ml
moved hard coded uris to HelmLibraryObjects
[helm.git] / helm / ocaml / tactics / tacticals.ml
index d499acb9ad2cb8a1ed70119d05a6c629f659edc0..57660310badd2935b53972670170313f3816b27f 100644 (file)
@@ -68,8 +68,8 @@ let rec try_tactics ~(tactics: (string * tactic) list) ~status =
         e ->
          match e with
             (Fail _)
-          | (CicTypeChecker.TypeCheckerFailure (CicTypeChecker.NotWellTyped _))
-          | (CicUnification.UnificationFailed) ->
+          | (CicTypeChecker.TypeCheckerFailure _)
+          | (CicUnification.UnificationFailure _) ->
               warn (
                 "Tacticals.try_tactics failed with exn: " ^
                 Printexc.to_string e);