aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacentries.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-04-23 16:19:43 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-04-23 16:19:43 +0200
commit5c34cfa54ec1959758baa3dd283e2e30853380db (patch)
treebe7c3a478307fc000f04e55f34e670d4dafcc451 /vernac/vernacentries.ml
parentd8532c76d8e758f95a5dcc36e0c9bc5fd144be16 (diff)
parent79ff2bc044aa86a5ce30f0c24647db8c8e2544fa (diff)
Merge PR #7152: [api] Remove dependency of library on Vernacexpr.
Diffstat (limited to 'vernac/vernacentries.ml')
-rw-r--r--vernac/vernacentries.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a9d1631ba..19658806c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -672,7 +672,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
else (idl,ty)) binders_ast in
let mp =
Declaremods.declare_module Modintern.interp_module_ast
- id binders_ast (Enforce mty_ast) []
+ id binders_ast (Declaremods.Enforce mty_ast) []
in
Dumpglob.dump_moddef ?loc mp "mod";
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");