- bug fixed: some liftings were missing in the implementation of rewrite

[helm.git] / helm / gTopLevel / fourierR.ml

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index d2725ff158fb49ee3445e1a615d7d4e0d0aa27d4..c46973e2cbeffab6cffc4a95224136ffb4603d07 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -57,7 +57,8 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
      let t1' = CicSubstitution.lift 1 t1 in
      let gty'' =
       ProofEngineReduction.replace_lifting
-       ~equality:ProofEngineReduction.syntactic_equality
+       ~equality:
+        (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true)
        ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
      in
       C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')