X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=aab75e9410dc1cf1823381e49fc1ed00428b8505;hb=38cd254c533f37e91677571dabd7587b7dc7dd28;hp=1708ed5b8e2d382ee10410c064c6af0b5c092dbf;hpb=32d6065811881d4ceac52448330ae793840e14e8;p=helm.git

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 1708ed5b8..aab75e941 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -678,7 +678,7 @@ let build_goal_proof l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-  (*canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty))*)proof, se
+  canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), se
 ;;
 
 let refl_proof ty term =