diff options
| author | Emilio Jesus Gallego Arias | 2018-11-08 13:17:14 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-21 01:25:23 +0100 |
| commit | 002a974b66bc5b8524c8c045d6b9ec4f57aa7734 (patch) | |
| tree | 573aec1d41d6dc4f8cb61f8fa0826ed9f27e6709 /parsing | |
| parent | 968be14b3788e112425eedf696f2e5e35d35ba17 (diff) | |
[gramlib] [build] Switch make-based system to packed gramlib
This makes the make-based build system stop linking to Camlp5's
gramlib and instead links to our own gramlib.
We use the style done in the packing of `Stdlib` in OCaml 4.07.
As to introduce a minimal amount of noise in history we use an
autogenerated `gramlib__pack` directory.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/cLexer.ml | 1 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 2 | ||||
| -rw-r--r-- | parsing/dune | 1 | ||||
| -rw-r--r-- | parsing/extend.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
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 *) |