From 8700a289dc58413cb0a44a51108b627aa5b3407e 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 --- helm/software/components/tactics/paramodulation/equality.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 3ac57e6fe..91ed61cd5 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/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