From: Enrico Tassi 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: make_still_working~7283 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1dd47a774f7e05e98323c4bd8629567574db47d2;p=helm.git 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 1708ed5b8..aab75e941 100644 --- 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 =