All the reduction tactics have been modified to reduce several (sub)terms

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 29df82c08ab5f21f121a688231ecf98d46058836..c1212360c96d0c1702b0055ff6a51417dd691dc3 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -81,7 +81,7 @@ let rewrite_simpl_tac ~term ~status =
  Tacticals.then_ 
   ~start:(rewrite_tac ~term)
   ~continuation:
-   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
+   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
   ~status
 ;;
 
@@ -144,7 +144,7 @@ let rewrite_back_simpl_tac ~term ~status =
  Tacticals.then_ 
   ~start:(rewrite_back_tac ~term)
   ~continuation:
-   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
+   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
   ~status
 ;;