1. rewrite_* and rewrite_back_* merged into one function

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 94f62a955a5297dd2a57c4896185053cbc46b08b..5bbfa33a6f3d27fb04ee3f39401bf5c165e933f5 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -24,7 +24,8 @@
  *)
  
 
-let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
+let rewrite_tac ~direction ~pattern equality =
+ let rewrite_tac ~direction ~pattern equality status =
 (*
   let module C = Cic in
   let module U = UriManager in
@@ -33,6 +34,7 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
   let module PEH = ProofEngineHelpers in
   let module PT = PrimitiveTactics in
   let module HLO = HelmLibraryObjects in
+  let proof,goal = status in
   let if_left a b = 
     match direction with
     | `Right -> b
@@ -106,45 +108,22 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
   in
   assert (List.length goals = 0) ;
   (proof',[fresh_meta])
-*) assert false
+  ProofEngineTypes.mk_tactic (rewrite_tac ?where ~term)
+*) assert false in
+ ProofEngineTypes.mk_tactic (rewrite_tac ~direction ~pattern equality)
   
  
-let rewrite_tac ?where ~term () =
-  let rewrite_tac ?where ~term status =
-    rewrite ?where ~term ~direction:`Right status
-  in
-  ProofEngineTypes.mk_tactic (rewrite_tac ?where ~term)
-
-let rewrite_simpl_tac ?where ~term () =
- let rewrite_simpl_tac ?where ~term status =
+let rewrite_simpl_tac ~direction ~pattern equality =
+ let rewrite_simpl_tac ~direction ~pattern equality status =
   ProofEngineTypes.apply_tactic
   (Tacticals.then_ 
-   ~start:(rewrite_tac ?where ~term ())
+   ~start:(rewrite_tac ~direction:`LeftToRight ~pattern equality)
    ~continuation:
      (ReductionTactics.simpl_tac
        ~pattern:(ProofEngineTypes.conclusion_pattern None)))
    status
  in
-   ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
-;;
-
-let rewrite_back_tac ?where ~term () =
-  let rewrite_back_tac ?where ~term status =
-    rewrite ?where ~term ~direction:`Left status
-  in
-  ProofEngineTypes.mk_tactic (rewrite_back_tac ?where ~term)
-
-let rewrite_back_simpl_tac ?where ~term () =
- let rewrite_back_simpl_tac ?where ~term status =
-  ProofEngineTypes.apply_tactic
-   (Tacticals.then_ 
-    ~start:(rewrite_back_tac ?where ~term ())
-    ~continuation:
-     (ReductionTactics.simpl_tac
-       ~pattern:(ProofEngineTypes.conclusion_pattern None)))
-   status
- in
-  ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term)
+   ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~direction ~pattern equality)
 ;;
 
 let replace_tac ~pattern ~with_what =