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 57c9805139a6a3c4aaa8d9440fda0ba181fd4290..a5c7878c7341336a822e39587adcaa5947b9d018 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -23,9 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*
+
 module PEH = ProofEngineHelpers 
-*)
 module U  = CicUniv
 module TC = CicTypeChecker 
 module PET = ProofEngineTypes 
@@ -37,10 +36,9 @@ module MI = CicMkImplicit
 module PESR = ProofEngineStructuralRules
 
 let fail_msg0 = "unexported clearbody: invalid argument"
-let fail_msg1 = "fwd: argument is not premise in the current goal"
 let fail_msg2 = "fwd: no applicable simplification"
 
-let error msg = raise (PET.Fail msg)
+let error msg = raise (PET.Fail (lazy msg))
 
 (* unexported tactics *******************************************************)
 
@@ -106,9 +104,11 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
       let lemma = FNG.clean_dummy_dependent_types lemma in
       let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in      
-      let conclusion =  Cic.Appl (what :: List.rev metas) in
-      let tac = T.thens ~start:(letin_tac conclusion)
-                       ~continuations:[clearbody ~index:1]
+      let conclusion =  
+         match metas with [] -> what | _ -> Cic.Appl (what :: List.rev metas)
+      in
+      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) = 
@@ -122,20 +122,8 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
 (* fwd **********************************************************************)
 
 let fwd_simpl_tac
-     ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
-     ~dbd hyp
-  =
-   let find_type metasenv context =
-      let rec aux p = function
-         | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t
-         | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t
-         | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
-            p, fst (TC.type_of_aux' metasenv tail u U.empty_ugraph)
-         | _ :: tail -> aux (succ p) tail
-         | [] -> error fail_msg1
-      in
-      aux 1 context
-   in
+     ?(mk_fresh_name_callback = FNG.mk_fresh_name ~subst:[])
+     ~dbd hyp =
    let lapply_tac to_what lemma = 
       lapply_tac ~mk_fresh_name_callback ~how_many:1 ~to_what:[to_what] lemma
    in
@@ -143,13 +131,13 @@ let fwd_simpl_tac
       let (proof, goal) = status in
       let _, metasenv, _, _ = proof in
       let _, context, ty = CicUtil.lookup_meta goal metasenv in
-      let index, major = find_type metasenv context in 
+      let index, major = PEH.lookup_type metasenv context hyp in 
       match MetadataQuery.fwd_simpl ~dbd major with
          | []       -> error fail_msg2
          | 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