X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=5f0ba8aaa97ee00f7c085f70386e17b5244e3484;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=0885f3037ffdcc1dfb9493ec1214f22f09b77022;hpb=d7a329578a475af98aa5f2a16d9873a576dab599;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 0885f3037..5f0ba8aaa 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -224,7 +224,8 @@ let fold term =
    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
    let replace =
     ProofEngineReduction.replace
-     ~equality:(ProofEngineReduction.syntactic_equality)
+     ~equality:
+      (ProofEngineReduction.syntactic_equality ~alpha_equivalence:false)
      ~what:term' ~with_what:term
    in
     let ty' = replace ty in
@@ -273,4 +274,4 @@ let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)
 let elim_type term = apply_tactic (Ring.elim_type_tac ~term)
 let ring () = apply_tactic Ring.ring_tac
 let fourier () = apply_tactic FourierR.fourier_tac
-let rewrite term = apply_tactic (FourierR.rewrite_tac ~term)
+let rewrite_simpl term = apply_tactic (FourierR.rewrite_simpl_tac ~term)