1. new syntax for patterns:

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index b9db6f705777eb9ae7acb09bace47a5cc6b1857c..94f62a955a5297dd2a57c4896185053cbc46b08b 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -25,6 +25,7 @@
  
 
 let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
+(*
   let module C = Cic in
   let module U = UriManager in
   let module PET = ProofEngineTypes in
@@ -105,6 +106,7 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
   in
   assert (List.length goals = 0) ;
   (proof',[fresh_meta])
+*) assert false
   
  
 let rewrite_tac ?where ~term () =
@@ -119,7 +121,8 @@ let rewrite_simpl_tac ?where ~term () =
   (Tacticals.then_ 
    ~start:(rewrite_tac ?where ~term ())
    ~continuation:
-     (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern))
+     (ReductionTactics.simpl_tac
+       ~pattern:(ProofEngineTypes.conclusion_pattern None)))
    status
  in
    ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
@@ -137,7 +140,8 @@ let rewrite_back_simpl_tac ?where ~term () =
    (Tacticals.then_ 
     ~start:(rewrite_back_tac ?where ~term ())
     ~continuation:
-     (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern))
+     (ReductionTactics.simpl_tac
+       ~pattern:(ProofEngineTypes.conclusion_pattern None)))
    status
  in
   ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term)