diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a494a10cc1..b897a6d919 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -10,6 +10,7 @@ open Pp open Errors +open Util open Flags open System open Vernacexpr |