aboutsummaryrefslogtreecommitdiff
path: root/plugins/interface/vtp.mli
diff options
context:
space:
mode:
authorletouzey2009-03-20 01:22:58 +0000
committerletouzey2009-03-20 01:22:58 +0000
commit7d220f8b61649646692983872626d6a8042446a9 (patch)
treefefceb2c59cf155c55fffa25ad08bec629de523e /plugins/interface/vtp.mli
parentad1fea78e3c23c903b2256d614756012d5f05d87 (diff)
Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface/vtp.mli')
-rw-r--r--plugins/interface/vtp.mli16
1 files changed, 16 insertions, 0 deletions
diff --git a/plugins/interface/vtp.mli b/plugins/interface/vtp.mli
new file mode 100644
index 0000000000..d7bd8db53c
--- /dev/null
+++ b/plugins/interface/vtp.mli
@@ -0,0 +1,16 @@
+open Ascent;;
+open Pp;;
+
+val fCOMMAND_LIST : ct_COMMAND_LIST -> std_ppcmds;;
+val fCOMMAND : ct_COMMAND -> std_ppcmds;;
+val fTACTIC_COM : ct_TACTIC_COM -> std_ppcmds;;
+val fFORMULA : ct_FORMULA -> std_ppcmds;;
+val fID : ct_ID -> std_ppcmds;;
+val fSTRING : ct_STRING -> std_ppcmds;;
+val fINT : ct_INT -> std_ppcmds;;
+val fRULE_LIST : ct_RULE_LIST -> std_ppcmds;;
+val fRULE : ct_RULE -> std_ppcmds;;
+val fSIGNED_INT_LIST : ct_SIGNED_INT_LIST -> std_ppcmds;;
+val fPREMISES_LIST : ct_PREMISES_LIST -> std_ppcmds;;
+val fID_LIST : ct_ID_LIST -> std_ppcmds;;
+val fTEXT : ct_TEXT -> std_ppcmds;;