now we use rplace_lifting_csc since the what must NOT be lifted

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index e1a4c6849d1c8507043dc466bf1efacb20205992..dd2c42f1cceb001f90f1d625b985cdeb9465a23a 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -84,7 +84,7 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
     aux (List.length what)
   in
   let gty'' =
-   ProofEngineReduction.replace_lifting
+   ProofEngineReduction.replace_lifting_csc 0
     ~equality:eq_kind ~what ~with_what ~where:gty'
   in
   let gty_red = CicSubstitution.subst t2 gty'' in