diff options
| author | lmamane | 2007-01-10 15:44:44 +0000 |
|---|---|---|
| committer | lmamane | 2007-01-10 15:44:44 +0000 |
| commit | bce104e3bb510fb10df2ecddebb47514328f2b8d (patch) | |
| tree | 69b2d6f827128ec3a769f3af9e58ffd8a6670b22 /contrib/interface/vtp.mli | |
| parent | fa49da538d1d65f34d7b7fd3c32e51ef7ff578a3 (diff) | |
Merge from Lionel Elie Mamane's private branch:
- Makefile: Option (environment variable NO_RECOMPILE_LIB) to not
recompile the whole standard library just because the coq binaries
got rebuilt.
- Infrastructure to change the object pretty-printers at runtime.
- Use that infrastructure to make coqtop-protocol with Pcoq trees and
Pcoq-protocol with pretty-printed terms possible in coq-interface.
- Make "Back(track)" into closed sections, modules and module types
"Just Workâ˘".
- Modernise/generalise Pcoq protocol a bit, make some of its warts
optional.
- Implement "Show." in Pcoq mode.
- Add Rpow_def.vo to REALSBASEVO so that its dependencies are
computed (and used).
- "make revision" now handles GNU Arch / tla in addition to svn.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/vtp.mli')
| -rw-r--r-- | contrib/interface/vtp.mli | 27 |
1 files changed, 14 insertions, 13 deletions
diff --git a/contrib/interface/vtp.mli b/contrib/interface/vtp.mli index fe30b317a7..d7bd8db53c 100644 --- a/contrib/interface/vtp.mli +++ b/contrib/interface/vtp.mli @@ -1,15 +1,16 @@ open Ascent;; +open Pp;; -val fCOMMAND_LIST : ct_COMMAND_LIST -> unit;; -val fCOMMAND : ct_COMMAND -> unit;; -val fTACTIC_COM : ct_TACTIC_COM -> unit;; -val fFORMULA : ct_FORMULA -> unit;; -val fID : ct_ID -> unit;; -val fSTRING : ct_STRING -> unit;; -val fINT : ct_INT -> unit;; -val fRULE_LIST : ct_RULE_LIST -> unit;; -val fRULE : ct_RULE -> unit;; -val fSIGNED_INT_LIST : ct_SIGNED_INT_LIST -> unit;; -val fPREMISES_LIST : ct_PREMISES_LIST -> unit;; -val fID_LIST : ct_ID_LIST -> unit;; -val fTEXT : ct_TEXT -> unit;;
\ No newline at end of file +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;; |