diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index ccbaa6d306..ca4a82ea69 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -32,6 +32,7 @@ open Pretyping open Redexpr open Syntax_def open Lemmas +open Declaremods (* Pcoq hooks *) |