From 0318a75de15f587bcbdb838984e8e59c913ec85c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 24 Jun 2005 17:20:47 +0000
Subject: [PATCH] now we use rplace_lifting_csc since the what must NOT be
 lifted

---
 helm/ocaml/tactics/equalityTactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index e1a4c6849..dd2c42f1c 100644
--- 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
-- 
2.39.2