From 2702434e5d6385b792e17218f473803e44177a3d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Jun 2006 15:52:18 +0000 Subject: [PATCH] pretty proofs are back --- components/tactics/paramodulation/equality.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 3ac57e6fe..91ed61cd5 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -736,9 +736,7 @@ let build_goal_proof eq l initial ty se = cic, p)) lets (letsno-1,initial) in -(* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), - * *) -proof, + canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), se ;; -- 2.39.2