diff options
Diffstat (limited to 'grammar/vernacextend.ml4')
| -rw-r--r-- | grammar/vernacextend.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 3074337f6..db8c51386 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -10,9 +10,7 @@ open Pp open Util -open Genarg open Q_util -open Q_coqast open Argextend open Tacextend open Pcoq |