]> matita.cs.unibo.it Git - helm.git/commitdiff
canonical and contextualize_rewrites are back, they seem to work now...
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 30 May 2006 09:09:37 +0000 (09:09 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 30 May 2006 09:09:37 +0000 (09:09 +0000)
components/tactics/paramodulation/equality.ml

index 1708ed5b8e2d382ee10410c064c6af0b5c092dbf..aab75e9410dc1cf1823381e49fc1ed00428b8505 100644 (file)
@@ -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 =