summaryrefslogtreecommitdiff
path: root/contrib/interface/showproof.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/showproof.mli')
-rwxr-xr-xcontrib/interface/showproof.mli23
1 files changed, 23 insertions, 0 deletions
diff --git a/contrib/interface/showproof.mli b/contrib/interface/showproof.mli
new file mode 100755
index 00000000..ee269458
--- /dev/null
+++ b/contrib/interface/showproof.mli
@@ -0,0 +1,23 @@
+open Environ
+open Evd
+open Names
+open Term
+open Util
+open Proof_type
+open Coqast
+open Pfedit
+open Translate
+open Term
+open Reduction
+open Clenv
+open Typing
+open Inductive
+open Vernacinterp
+open Declarations
+open Showproof_ct
+open Proof_trees
+open Sign
+open Pp
+open Printer
+
+val show_proof : string -> int list -> Ascent.ct_TEXT;;