matitaprover

[helm.git] / helm / software / components / tactics / autoTactic.ml

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index d4dc5592c78379caa95f6d32fffd8af8d9f7b889..f063eeafb69ff99d7d49bf6b6810d6768f302e41 100644 (file)
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -494,3 +494,5 @@ let applyS_tac ~dbd ~term =
     | CicUnification.UnificationFailure msg
     | CicTypeChecker.TypeCheckerFailure msg ->
         raise (ProofEngineTypes.Fail msg))
+
+let pp_proofterm = Equality.pp_proofterm;;