diff options
Diffstat (limited to 'parsing/egrammar.mli')
| -rw-r--r-- | parsing/egrammar.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index c9f92b7294..108f39eaab 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -10,7 +10,8 @@ open Compat open Errors open Pp open Names -open Topconstr +open Constrexpr +open Notation_term open Pcoq open Extend open Vernacexpr |