X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=fc6413eb5ceb385d0056f9d6b978e8679216ac2c;hb=6bbeb650abc3a94e76d683aa47b2e46254d495d1;hp=51f28b3c9e7b6a29c634128afc87a7a37014d147;hpb=d1126c6b78a3333bbf415daf027004496b77c2f4;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 51f28b3c9..fc6413eb5 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 
 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
 chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
@@ -55,7 +57,7 @@ let assumption_tac =
 		 if b then n else find (n+1) tl
            | _ -> find (n+1) tl
          )
-      | [] -> raise (PET.Fail "Assumption: No such assumption")
+      | [] -> raise (PET.Fail (lazy "Assumption: No such assumption"))
      in PET.apply_tactic (PT.apply_tac ~term:(C.Rel (find 1 context))) status
  in
   PET.mk_tactic assumption_tac