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

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 1708ed5b8e2d382ee10410c064c6af0b5c092dbf..aab75e9410dc1cf1823381e49fc1ed00428b8505 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/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 =