aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/interface/showproof.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/interface/showproof.mli')
-rwxr-xr-xplugins/interface/showproof.mli21
1 files changed, 21 insertions, 0 deletions
diff --git a/plugins/interface/showproof.mli b/plugins/interface/showproof.mli
new file mode 100755
index 000000000..9b6787b7c
--- /dev/null
+++ b/plugins/interface/showproof.mli
@@ -0,0 +1,21 @@
+open Environ
+open Evd
+open Names
+open Term
+open Util
+open Proof_type
+open Pfedit
+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;;