replace_lifting generalized to the simultaneous replacement of n terms.

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 36704b441fdaee9f76d8603abfc1d47b5c008b39..8cb794ff6e17e918eefd4f0696276a41fc806822 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -56,7 +56,7 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
      let gty'' =
       ProofEngineReduction.replace_lifting
        ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
       C.Lambda
        (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
@@ -118,7 +118,7 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
      let gty'' =
       ProofEngineReduction.replace_lifting
        ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
       C.Lambda
        (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')