ocaml 3.09 transition

[helm.git] / helm / ocaml / tactics / fwdSimplTactic.ml

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index bd2ac9fdeb7d85861cb6f130879ba61ced2d9bd5..a5c7878c7341336a822e39587adcaa5947b9d018 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -38,7 +38,7 @@ module PESR = ProofEngineStructuralRules
 let fail_msg0 = "unexported clearbody: invalid argument"
 let fail_msg2 = "fwd: no applicable simplification"
 
-let error msg = raise (PET.Fail msg)
+let error msg = raise (PET.Fail (lazy msg))
 
 (* unexported tactics *******************************************************)
 
@@ -107,8 +107,8 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       let conclusion =  
          match metas with [] -> what | _ -> Cic.Appl (what :: List.rev metas)
       in
-      let tac = T.thens ~start:(letin_tac conclusion)
-                       ~continuations:[clearbody ~index:1]
+      let tac = T.then_ ~start:(letin_tac conclusion) 
+        ~continuation:(clearbody ~index:1)
       in
       let proof = (xuri, metasenv, u, t) in
       let aux (proof, goals) (tac, goal) = 
@@ -137,7 +137,7 @@ let fwd_simpl_tac
          | uri :: _ -> 
            Printf.eprintf "fwd: %s\n" (UriManager.string_of_uri uri); flush stderr;
            let start = lapply_tac (Cic.Rel index) (Cic.Const (uri, [])) in  
-            let tac = T.thens ~start ~continuations:[PESR.clear hyp] in
+            let tac = T.then_ ~start ~continuation:(PESR.clear hyp) in
             PET.apply_tactic tac status
    in
    PET.mk_tactic fwd_simpl_tac