From 1dd47a774f7e05e98323c4bd8629567574db47d2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 30 May 2006 09:09:37 +0000 Subject: [PATCH] canonical and contextualize_rewrites are back, they seem to work now... --- helm/software/components/tactics/paramodulation/equality.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 = -- 2.39.2