diff options
Diffstat (limited to 'vernac/comPrimitive.ml')
| -rw-r--r-- | vernac/comPrimitive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml index 06fafddafb..b66ff876d3 100644 --- a/vernac/comPrimitive.ml +++ b/vernac/comPrimitive.ml @@ -9,7 +9,7 @@ (************************************************************************) let do_primitive id prim typopt = - if Lib.sections_are_opened () then + if Global.sections_are_opened () then CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections."); if Dumpglob.dump () then Dumpglob.dump_definition id false "ax"; let env = Global.env () in |