6 files changed, 5 insertions, 3 deletions

diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 619718f723..d81ee475b5 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -11,6 +11,7 @@
 open Pp
 open Util
 open Tok
+open Gramlib
 
 (** Location utilities  *)
 let ploc_file_of_coq_file = function
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index e4aa8debc1..c0ebdd45ef 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -40,7 +40,7 @@ where
       tok_text : pattern -> string;
       tok_comm : mutable option (list location) }
  *)
-include Grammar.GLexerType with type te = Tok.t
+include Gramlib.Grammar.GLexerType with type te = Tok.t
 
 module Error : sig
   type t
diff --git a/parsing/dune b/parsing/dune
index 0669e3a3c2..e91740650f 100644
--- a/parsing/dune
+++ b/parsing/dune
@@ -2,7 +2,6 @@
  (name parsing)
  (public_name coq.parsing)
  (wrapped false)
- (flags :standard -open Gramlib)
  (libraries coq.gramlib proofs))
 
 (rule
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 6fe2956643..5caeab535a 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -10,7 +10,7 @@
 
 (** Entry keys for constr notations *)
 
-type 'a entry = 'a Grammar.GMake(CLexer).Entry.e
+type 'a entry = 'a Gramlib.Grammar.GMake(CLexer).Entry.e
 
 type side = Left | Right
 
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index d4aa598fd8..445338b786 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -12,6 +12,7 @@ open CErrors
 open Util
 open Extend
 open Genarg
+open Gramlib
 
 let curry f x y = f (x, y)
 let uncurry f (x,y) = f x y
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index c05229d576..593cf59341 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -13,6 +13,7 @@ open Extend
 open Genarg
 open Constrexpr
 open Libnames
+open Gramlib
 
 (** The parser of Coq *)