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