]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/variousTactics.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / tactics / variousTactics.ml
index 51f28b3c9e7b6a29c634128afc87a7a37014d147..927552f0a60219c558dc35a38368541f90586ed7 100644 (file)
@@ -55,7 +55,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