From 4759f60b04a278ecd46c8a120340ba55b185c6d1 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 16 Dec 2013 17:08:46 +0100
Subject: A few fixes to the build system (mostly for ocamlbuild)

 * vars.mli was mentionning Term instead of Constr, leading to a dep cycle
 * Having a file named toplevel/toplevel.ml isn't a good idea when we also
   have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
   We rename toplevel.ml into Coqloop.ml
 * Extra cleanup of toplevel.mllib :
   - Ppextra isn't anywhere around (?!)
   - Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
   - Vernacexpr is a .mli and shouldn't appear in an .mllib
 * During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
 * A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
   for coqchk).
---
 printing/ppvernac.ml    |  1 -
 printing/ppvernac.mli   | 18 ++----------------
 printing/printing.mllib |  1 +
 3 files changed, 3 insertions(+), 17 deletions(-)

(limited to 'printing')

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
-- 
cgit v1.2.3