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

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 8abaae1b849e67711982ba74a0a626a51e965e72..91cd6198ef8bb28d6d60f7a42a8450fdfa62bcc8 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -523,7 +523,7 @@ let elim_intros_simpl_tac ~term =
    (Tacticals.thens
      ~start:(intros_tac ())
      ~continuations:
-       [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None])
+       [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None])
 ;;
 
 exception NotConvertible
@@ -540,7 +540,8 @@ let change_tac ~what ~with_what ~status:(proof, goal) =
   if CicReduction.are_convertible context what with_what then
    begin
     let replace =
-     ProofEngineReduction.replace ~equality:(==) ~what ~with_what
+     ProofEngineReduction.replace
+      ~equality:(==) ~what:[what] ~with_what:[with_what]
     in
     let ty' = replace ty in
     let context' =