diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 1 | ||||
| -rw-r--r-- | printing/ppvernac.mli | 18 | ||||
| -rw-r--r-- | printing/printing.mllib | 1 |
3 files changed, 3 insertions, 17 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index ba640863d0..4ece6cb24d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -9,7 +9,6 @@ open Pp open Names -(* open Compat *) open Errors open Util open Extend diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index 0e6eba2679..a3d0465a62 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -6,22 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Genarg -open Vernacexpr -open Names -open Nameops -open Nametab -open Ppconstr -open Pptactic -open Glob_term -open Pcoq -open Libnames -open Ppextend -open Topconstr - (** Prints a vernac expression *) -val pr_vernac_body : vernac_expr -> std_ppcmds +val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds (** Prints a vernac expression and closes it with a dot. *) -val pr_vernac : vernac_expr -> std_ppcmds +val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds diff --git a/printing/printing.mllib b/printing/printing.mllib index 9b3bffc8d6..2a8f1030fe 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -5,3 +5,4 @@ Printer Pptactic Printmod Prettyp +Ppvernac |