diff options
Diffstat (limited to 'parsing/ppvernac.mli')
| -rw-r--r-- | parsing/ppvernac.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli index 6d83ca474..91bb19a8c 100644 --- a/parsing/ppvernac.mli +++ b/parsing/ppvernac.mli @@ -12,6 +12,7 @@ open Vernacexpr open Names open Nameops open Nametab +open Errors open Util open Ppconstr open Pptactic |