From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 30 May 2006 09:09:37 +0000 (+0000)
Subject: canonical and contextualize_rewrites are back, they seem to work now...
X-Git-Tag: 0.4.95@7852~1386
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=38cd254c533f37e91677571dabd7587b7dc7dd28;hp=32d6065811881d4ceac52448330ae793840e14e8;p=helm.git

canonical and contextualize_rewrites are back, they seem to work now...
---

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 =