diff options
Diffstat (limited to 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index d72a06f2a..67322863a 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -13,7 +13,6 @@ open Util open Ast open Genarg open Tacexpr -open Vernacexpr (* The lexer of Coq *) @@ -75,6 +74,7 @@ type typed_entry = entry_type Gramobj.entry module type Gramtypes = sig + open Decl_kinds val inAstListType : Coqast.t list G.Entry.e -> typed_entry val inTacticAtomAstType : raw_atomic_tactic_expr G.Entry.e -> typed_entry val inThmTokenAstType : theorem_kind G.Entry.e -> typed_entry |