diff options
| author | Pierre-Marie Pédrot | 2016-02-17 13:45:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-19 01:17:39 +0100 |
| commit | 805c8987fbb5fdeb94838bb5a3a7364c0a3d3374 (patch) | |
| tree | 847bc8e25c550394991eee31aba854667f0b60e7 /parsing/egramml.ml | |
| parent | a99aa093b962e228817066d00f7e12698f8df73a (diff) | |
Do not export entry_key from Pcoq anymore.
Diffstat (limited to 'parsing/egramml.ml')
| -rw-r--r-- | parsing/egramml.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 77252e7425..37fccdb3c2 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -9,6 +9,7 @@ open Util open Compat open Names +open Extend open Pcoq open Genarg open Vernacexpr @@ -18,7 +19,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : - Loc.t * 'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's grammar_prod_item + Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item type 'a ty_arg = ('a -> raw_generic_argument) |