From 79ff2bc044aa86a5ce30f0c24647db8c8e2544fa Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
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.
---
 parsing/g_vernac.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 593dcbf58c..2dbd624c2c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -17,6 +17,7 @@ open Constrexpr
 open Constrexpr_ops
 open Extend
 open Decl_kinds
+open Declaremods
 open Declarations
 open Misctypes
 open Tok (* necessary for camlp5 *)
-- 
cgit v1.2.3