X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=91ed61cd5ea9426b7e111029a1e68cf84625f784;hb=8700a289dc58413cb0a44a51108b627aa5b3407e;hp=3ac57e6fe63ed2285b06722d7e7dd04853cf298f;hpb=1d8438e80bbbd6c9b15e3beeba17af9d12b702c5;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 3ac57e6fe..91ed61cd5 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -736,9 +736,7 @@ let build_goal_proof eq l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-(*    canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
- *    *)
-proof,
+   canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
    se 
 ;;