From 79ff2bc044aa86a5ce30f0c24647db8c8e2544fa Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 2 Apr 2018 04:26:09 +0200
Subject: [api] Remove dependency of library on Vernacexpr.

Morally, `library` should not depend on the vernacular
definition. This will also create problems when trying to modularize
the codebase due to the cycle [vernacs depend for example on
constrexprs].

The fix is fortunately easy.
---
 printing/ppvernac.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 7eb8396ac..83c875707 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -16,12 +16,13 @@ open Util
 open CAst
 
 open Extend
-open Vernacexpr
-open Pputils
 open Libnames
+open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
-open Decl_kinds
+open Vernacexpr
+open Declaremods
+open Pputils
 
   open Ppconstr
 
-- 
cgit v1.2.3