diff options
Diffstat (limited to 'parsing/extend.ml')
| -rw-r--r-- | parsing/extend.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml index fca24ed5a..22d640f50 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -7,6 +7,7 @@ (************************************************************************) open Compat +open Errors open Util (** Entry keys for constr notations *) |