fixed proof generation again

[helm.git] / helm / software / components / tactics / paramodulation / equality.ml

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index aab75e9410dc1cf1823381e49fc1ed00428b8505..52918d9af1359017f94b3ffd4b6e6af5f534d528 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -678,7 +678,8 @@ let build_goal_proof l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-  canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), se
+  canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), 
+   se
 ;;
 
 let refl_proof ty term =