diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 5d12af054..147c5261d 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Errors open Names open Glob_term open Extend @@ -156,7 +155,6 @@ val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> module Prim : sig - open Util open Names open Libnames val preident : string Gram.entry |