]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/primitiveTactics.ml
Every exception that used to have type string is now a string Lazy.t.
[helm.git] / helm / ocaml / tactics / primitiveTactics.ml
index 74a9f63f2548290bb22e136e58cf9ae2f9ee06f2..d26221d3951bac5c6e82bf3437ffbaf3fba6477c 100644 (file)
@@ -67,7 +67,7 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name =
          in
           context, t, (C.Meta (newmeta,irl))
         else
-         raise (Fail "intro(s): not enough products or let-ins")
+         raise (Fail (lazy "intro(s): not enough products or let-ins"))
   in
    collect_context context howmany ty 
 
@@ -325,10 +325,9 @@ let apply_tac_verbose_with_subst ~term status =
     apply_tac_verbose_with_subst ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with 
-  | CicUnification.UnificationFailure msg -> 
-      raise (Fail (CicUnification.explain_error msg))
-  | CicTypeChecker.TypeCheckerFailure _ as e ->
-      raise (Fail (Printexc.to_string e))
+  | CicUnification.UnificationFailure msg
+  | CicTypeChecker.TypeCheckerFailure msg ->
+      raise (Fail msg)
 
 (* ALB *)
 let apply_tac_verbose ~term status =
@@ -345,10 +344,9 @@ let apply_tac ~term =
     apply_tac ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with 
-  | CicUnification.UnificationFailure msg ->
-      raise (Fail (CicUnification.explain_error msg))
-  | CicTypeChecker.TypeCheckerFailure _ as e ->
-      raise (Fail (Printexc.to_string e))
+  | CicUnification.UnificationFailure msg
+  | CicTypeChecker.TypeCheckerFailure msg ->
+      raise (Fail msg)
  in
   mk_tactic (apply_tac ~term)
 
@@ -453,7 +451,7 @@ let exact_tac ~term =
     (newproof, [])
    end
   else
-   raise (Fail "The type of the provided term is not the one expected.")
+   raise (Fail (lazy "The type of the provided term is not the one expected."))
  in
   mk_tactic (exact_tac ~term)