diff options
Diffstat (limited to 'plugins/ltac/pltac.mli')
| -rw-r--r-- | plugins/ltac/pltac.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 810e1ec39..9261a11c7 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -8,6 +8,8 @@ (** Ltac parsing entries *) +open API +open Grammar_API open Loc open Names open Pcoq |