diff options
Diffstat (limited to 'parsing/egramml.ml')
| -rw-r--r-- | parsing/egramml.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/egramml.ml b/parsing/egramml.ml index dc558e841..f26ff817b 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -10,7 +10,6 @@ open Compat open Names open Pcoq open Genarg -open Tacexpr open Vernacexpr (** Making generic actions in type generic_argument *) |