aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/safe_typing.ml19
-rw-r--r--kernel/safe_typing.mli6
-rw-r--r--kernel/section.ml2
-rw-r--r--kernel/section.mli3
-rw-r--r--library/global.ml5
-rw-r--r--library/global.mli6
-rw-r--r--library/lib.ml16
-rw-r--r--library/lib.mli1
-rw-r--r--library/nametab.ml2
-rw-r--r--library/nametab.mli1
-rw-r--r--plugins/extraction/table.ml2
-rw-r--r--printing/printmod.ml2
-rw-r--r--tactics/declare.ml9
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comPrimitive.ml2
-rw-r--r--vernac/declaremods.ml14
-rw-r--r--vernac/locality.ml6
-rw-r--r--vernac/vernacentries.ml14
18 files changed, 59 insertions, 53 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9b4d2e69ac..fc55720583 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -173,6 +173,8 @@ let is_initial senv =
| [], NONE -> ModPath.equal senv.modpath ModPath.initial
| _ -> false
+let sections_are_opened senv = not (Section.is_empty senv.sections)
+
let delta_of_senv senv = senv.modresolver,senv.paramresolver
let constant_of_delta_kn_senv senv kn =
@@ -587,10 +589,10 @@ type global_declaration =
type exported_private_constant = Constant.t
-let add_constant_aux ~in_section senv (kn, cb) =
+let add_constant_aux senv (kn, cb) =
let l = Constant.label kn in
(* This is the only place where we hashcons the contents of a constant body *)
- let cb = if in_section then cb else Declareops.hcons_const_body cb in
+ let cb = if sections_are_opened senv then cb else Declareops.hcons_const_body cb in
let senv' = add_field (l,SFBconst cb) (C kn) senv in
let senv'' = match cb.const_body with
| Undef (Some lev) ->
@@ -799,7 +801,7 @@ let push_opaque_proof pf senv =
let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
senv, o
-let export_private_constants ~in_section ce senv =
+let export_private_constants ce senv =
let exported, ce = export_side_effects senv.revstruct senv.env ce in
let map senv (kn, c) = match c.const_body with
| OpaqueDef p ->
@@ -815,10 +817,10 @@ let export_private_constants ~in_section ce senv =
let senv, bodies = List.fold_left_map map senv exported in
let exported = List.map (fun (kn, _) -> kn) exported in
(* No delayed constants to declare *)
- let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
+ let senv = List.fold_left add_constant_aux senv bodies in
(ce, exported), senv
-let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment =
+let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constant.t * a) * safe_environment =
let kn = Constant.make2 senv.modpath l in
let cb =
match decl with
@@ -852,14 +854,14 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
| Undef _ | Def _ | Primitive _ as body ->
senv, { cb with const_body = body }, []
in
- let senv = add_constant_aux ~in_section senv (kn, cb) in
+ let senv = add_constant_aux senv (kn, cb) in
add_constraints_list delayed_cst senv
in
let senv =
match decl with
| ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) ->
- if in_section then CErrors.anomaly (Pp.str "Primitive type not allowed in sections");
+ if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections");
add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
| _ -> senv
in
@@ -1001,12 +1003,11 @@ let close_section senv =
in
let fold senv = function
| `Definition (kn, cb) ->
- let in_section = not (Section.is_empty senv.sections) in
let info = cooking_info (Section.segment_of_constant env0 kn sections0) in
let r = { Cooking.from = cb; info } in
let cb = Term_typing.translate_recipe senv.env kn r in
(* Delayed constants are already in the global environment *)
- add_constant_aux ~in_section senv (kn, cb)
+ add_constant_aux senv (kn, cb)
| `Inductive (ind, mib) ->
let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
let mie = Cooking.cook_inductive info mib in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index d97d61a72f..1b55293f1c 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -82,13 +82,13 @@ type global_declaration =
type exported_private_constant = Constant.t
-val export_private_constants : in_section:bool ->
+val export_private_constants :
private_constants Entries.proof_output ->
(Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
(** returns the main constant plus a certificate of its validity *)
val add_constant :
- side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration ->
+ side_effect:'a effect_entry -> Label.t -> global_declaration ->
(Constant.t * 'a) safe_transformer
(** Adding an inductive type *)
@@ -138,6 +138,8 @@ val open_section : safe_transformer0
val close_section : safe_transformer0
+val sections_are_opened : safe_environment -> bool
+
(** Insertion of local declarations (Local or Variables) *)
val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
diff --git a/kernel/section.ml b/kernel/section.ml
index babd9fe7a1..a1242f0faf 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -43,6 +43,8 @@ let empty = []
let is_empty = List.is_empty
+let depth = List.length
+
let has_poly_univs = function
| [] -> false
| sec :: _ -> sec.has_poly_univs
diff --git a/kernel/section.mli b/kernel/section.mli
index 56b4d9ba8f..ec863b3b90 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -21,6 +21,9 @@ val empty : 'a t
val is_empty : 'a t -> bool
(** Checks whether there is no opened section *)
+val depth : 'a t -> int
+(** Number of nested sections (0 if no sections are open) *)
+
(** {6 Manipulating sections} *)
type section_entry =
diff --git a/library/global.ml b/library/global.ml
index c4685370d1..24cfc57f28 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -102,8 +102,8 @@ let typing_flags () = Environ.typing_flags (env ())
let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
let sprop_allowed () = Environ.sprop_allowed (env())
-let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
-let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d)
+let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
+let add_constant ~side_effect id d = globalize (Safe_typing.add_constant ~side_effect (i2l id) d)
let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
@@ -111,6 +111,7 @@ let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
let open_section () = globalize0 Safe_typing.open_section
let close_section fs = globalize0_with_summary fs Safe_typing.close_section
+let sections_are_opened () = Safe_typing.sections_are_opened (safe_env())
let start_module id = globalize (Safe_typing.start_module (i2l id))
let start_modtype id = globalize (Safe_typing.start_modtype (i2l id))
diff --git a/library/global.mli b/library/global.mli
index c45bf65d84..d689771f0a 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -46,12 +46,12 @@ val push_named_assum : (Id.t * Constr.types) -> unit
val push_named_def : (Id.t * Entries.section_def_entry) -> unit
val push_section_context : (Name.t array * Univ.UContext.t) -> unit
-val export_private_constants : in_section:bool ->
+val export_private_constants :
Safe_typing.private_constants Entries.proof_output ->
Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
val add_constant :
- side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a
+ side_effect:'a Safe_typing.effect_entry -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a
val add_mind :
Id.t -> Entries.mutual_inductive_entry -> MutInd.t
@@ -80,6 +80,8 @@ val close_section : Summary.frozen -> unit
(** Close the section and reset the global state to the one at the time when
the section what opened. *)
+val sections_are_opened : unit -> bool
+
(** Interactive modules and module types *)
val start_module : Id.t -> ModPath.t
diff --git a/library/lib.ml b/library/lib.ml
index 0d9efe2d5d..80b50b26d0 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -107,7 +107,6 @@ let segment_of_objects prefix =
let initial_prefix = Nametab.{
obj_dir = default_library;
obj_mp = ModPath.initial;
- obj_sec = DirPath.empty;
}
type lib_state = {
@@ -132,10 +131,10 @@ let library_dp () =
let cwd () = !lib_state.path_prefix.Nametab.obj_dir
let current_mp () = !lib_state.path_prefix.Nametab.obj_mp
-let current_sections () = !lib_state.path_prefix.Nametab.obj_sec
+let current_sections () = Safe_typing.sections_of_safe_env (Global.safe_env())
-let sections_depth () = List.length (Names.DirPath.repr (current_sections ()))
-let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ()))
+let sections_depth () = Section.depth (current_sections())
+let sections_are_opened = Global.sections_are_opened
let cwd_except_section () =
Libnames.pop_dirpath_n (sections_depth ()) (cwd ())
@@ -169,7 +168,6 @@ let pop_path_prefix () =
let op = !lib_state.path_prefix in
lib_state := { !lib_state
with path_prefix = Nametab.{ op with obj_dir = pop_dirpath op.obj_dir;
- obj_sec = pop_dirpath op.obj_sec;
} }
let find_entry_p p =
@@ -282,7 +280,7 @@ let current_mod_id () =
let start_mod is_type export id mp fs =
let dir = add_dirpath_suffix (!lib_state.path_prefix.Nametab.obj_dir) id in
- let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
+ let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; } in
let exists =
if is_type then Nametab.exists_cci (make_path id)
else Nametab.exists_dir dir
@@ -330,9 +328,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
let start_compilation s mp =
if !lib_state.comp_name != None then
user_err Pp.(str "compilation unit is already started");
- if not (Names.DirPath.is_empty (!lib_state.path_prefix.Nametab.obj_sec)) then
+ if Global.sections_are_opened () then (* XXX not sure if we need this check *)
user_err Pp.(str "some sections are already opened");
- let prefix = Nametab.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir = s; obj_mp = mp } in
add_anonymous_entry (CompilingLibrary prefix);
lib_state := { !lib_state with comp_name = Some s;
path_prefix = prefix }
@@ -465,7 +463,7 @@ let open_section id =
let () = Global.open_section () in
let opp = !lib_state.path_prefix in
let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
- let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
+ let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; } in
if Nametab.exists_dir obj_dir then
user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
let fs = Summary.freeze_summaries ~marshallable:false in
diff --git a/library/lib.mli b/library/lib.mli
index 59d77480e9..cef50a5f3b 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -95,6 +95,7 @@ val make_kn : Id.t -> KerName.t
(** Are we inside an opened section *)
val sections_are_opened : unit -> bool
+[@@ocaml.deprecated "Use Global.sections_are_opened"]
val sections_depth : unit -> int
(** Are we inside an opened module type *)
diff --git a/library/nametab.ml b/library/nametab.ml
index aed7d08ac1..8626ee1c59 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -18,12 +18,10 @@ open Globnames
type object_prefix = {
obj_dir : DirPath.t;
obj_mp : ModPath.t;
- obj_sec : DirPath.t;
}
let eq_op op1 op2 =
DirPath.equal op1.obj_dir op2.obj_dir &&
- DirPath.equal op1.obj_sec op2.obj_sec &&
ModPath.equal op1.obj_mp op2.obj_mp
(* to this type are mapped DirPath.t's in the nametab *)
diff --git a/library/nametab.mli b/library/nametab.mli
index 6ee22fc283..55458fe2c6 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -74,7 +74,6 @@ open Globnames
type object_prefix = {
obj_dir : DirPath.t;
obj_mp : ModPath.t;
- obj_sec : DirPath.t;
}
val eq_op : object_prefix -> object_prefix -> bool
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 96a3d00dc2..be9259861a 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -380,7 +380,7 @@ let check_inside_module () =
warn_extraction_inside_module ()
let check_inside_section () =
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
err (str "You can't do that within a section." ++ fnl () ++
str "Close it and try again.")
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 03921bca30..4cc6bc2052 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -213,7 +213,7 @@ let print_kn locals kn =
let nametab_register_dir obj_mp =
let id = mk_fake_top () in
let obj_dir = DirPath.make [id] in
- Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty }))
+ Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; }))
(** Nota: the [global_reference] we register in the nametab below
might differ from internal ones, since we cannot recreate here
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 3590146dfb..61321cd605 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -249,14 +249,13 @@ let is_unsafe_typing_flags () =
let define_constant ~side_effect ~name cd =
(* Logically define the constant and its subproofs, no libobject tampering *)
- let in_section = Lib.sections_are_opened () in
let export, decl, unsafe = match cd with
| DefinitionEntry de ->
(* We deal with side effects *)
if not de.proof_entry_opaque then
(* This globally defines the side-effects in the environment. *)
let body, eff = Future.force de.proof_entry_body in
- let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in
+ let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in
let export = get_roles export eff in
let de = { de with proof_entry_body = Future.from_val (body, ()) } in
let cd = Entries.DefinitionEntry (cast_proof_entry de) in
@@ -272,7 +271,7 @@ let define_constant ~side_effect ~name cd =
| PrimitiveEntry e ->
[], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false
in
- let kn, eff = Global.add_constant ~side_effect ~in_section name decl in
+ let kn, eff = Global.add_constant ~side_effect name decl in
if unsafe || is_unsafe_typing_flags() then feedback_axiom();
kn, eff, export
@@ -319,7 +318,7 @@ let declare_variable ~name ~kind d =
(* The body should already have been forced upstream because it is a
section-local definition, but it's not enforced by typing *)
let (body, eff) = Future.force de.proof_entry_body in
- let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in
+ let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in
let eff = get_roles export eff in
let () = List.iter register_side_effect eff in
let poly, univs = match de.proof_entry_universes with
@@ -585,7 +584,7 @@ let declare_univ_binders gr pl =
Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
let do_universe ~poly l =
- let in_section = Lib.sections_are_opened () in
+ let in_section = Global.sections_are_opened () in
let () =
if poly && not in_section then
CErrors.user_err ~hdr:"Constraint"
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 5ba8b0ab3c..f9b73a59eb 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -287,7 +287,7 @@ let context ~poly l =
name,b,t,impl)
ctx
in
- if Lib.sections_are_opened ()
+ if Global.sections_are_opened ()
then context_insection sigma ~poly ctx
else context_nosection sigma ~poly ctx
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
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 58a7dff5fd..c7b68d18c2 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -211,7 +211,7 @@ let compute_visibility exists i =
(** Iterate some function [iter_objects] on all components of a module *)
let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs =
- let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir ; obj_mp; } in
let dirinfo = Nametab.GlobDirRef.DirModule prefix in
consistency_checks exists obj_dir dirinfo;
Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo;
@@ -266,14 +266,14 @@ and load_objects i prefix objs =
and load_include i ((sp,kn), aobjs) =
let obj_dir = Libnames.dirpath sp in
let obj_mp = KerName.modpath kn in
- let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir; obj_mp; } in
let o = expand_aobjs aobjs in
load_objects i prefix o
and load_keep i ((sp,kn),kobjs) =
(* Invariant : seg isn't empty *)
let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
- let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir ; obj_mp; } in
let modobjs =
try ModObjs.get obj_mp
with Not_found -> assert false (* a substobjs should already be loaded *)
@@ -327,7 +327,7 @@ let rec open_object i (name, obj) =
| KeepObject objs -> open_keep i (name, objs)
and open_module i obj_dir obj_mp sobjs =
- let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir ; obj_mp; } in
let dirinfo = Nametab.GlobDirRef.DirModule prefix in
consistency_checks true obj_dir dirinfo;
Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo;
@@ -353,7 +353,7 @@ and open_modtype i ((sp,kn),_) =
and open_include i ((sp,kn), aobjs) =
let obj_dir = Libnames.dirpath sp in
let obj_mp = KerName.modpath kn in
- let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir; obj_mp; } in
let o = expand_aobjs aobjs in
open_objects i prefix o
@@ -363,7 +363,7 @@ and open_export i mpl =
and open_keep i ((sp,kn),kobjs) =
let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
- let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir; obj_mp; } in
open_objects i prefix kobjs
let rec cache_object (name, obj) =
@@ -380,7 +380,7 @@ let rec cache_object (name, obj) =
and cache_include ((sp,kn), aobjs) =
let obj_dir = Libnames.dirpath sp in
let obj_mp = KerName.modpath kn in
- let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir; obj_mp; } in
let o = expand_aobjs aobjs in
load_objects 1 prefix o;
open_objects 1 prefix o
diff --git a/vernac/locality.ml b/vernac/locality.ml
index f033d32874..5862f51b43 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -39,7 +39,7 @@ let enforce_locality_exp locality_flag discharge =
match locality_flag, discharge with
| Some b, NoDischarge -> Global (importability_of_bool b)
| None, NoDischarge -> Global Declare.ImportDefaultBehavior
- | None, DoDischarge when not (Lib.sections_are_opened ()) ->
+ | None, DoDischarge when not (Global.sections_are_opened ()) ->
(* If a Let/Variable is defined outside a section, then we consider it as a local definition *)
warn_local_declaration ();
Global Declare.ImportNeedQualified
@@ -55,7 +55,7 @@ let enforce_locality locality_flag =
Local in sections is the default, Local not in section forces non-export *)
let make_section_locality =
- function Some b -> b | None -> Lib.sections_are_opened ()
+ function Some b -> b | None -> Global.sections_are_opened ()
let enforce_section_locality locality_flag =
make_section_locality locality_flag
@@ -68,7 +68,7 @@ let enforce_section_locality locality_flag =
let make_module_locality = function
| Some false ->
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
CErrors.user_err Pp.(str
"This command does not support the Global option in sections.");
false
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4734ce1fb9..430cee62c2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -810,14 +810,14 @@ let vernac_combined_scheme lid l =
Indschemes.do_combined_scheme lid l
let vernac_universe ~poly l =
- if poly && not (Lib.sections_are_opened ()) then
+ if poly && not (Global.sections_are_opened ()) then
user_err ~hdr:"vernac_universe"
(str"Polymorphic universes can only be declared inside sections, " ++
str "use Monomorphic Universe instead");
Declare.do_universe ~poly l
let vernac_constraint ~poly l =
- if poly && not (Lib.sections_are_opened ()) then
+ if poly && not (Global.sections_are_opened ()) then
user_err ~hdr:"vernac_constraint"
(str"Polymorphic universe constraints can only be declared"
++ str " inside sections, use Monomorphic Constraint instead");
@@ -837,7 +837,7 @@ let vernac_import export refl =
let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
let binders_ast = List.map
(fun (export,idl,ty) ->
@@ -852,7 +852,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mexpr_ast_l with
| [] ->
@@ -893,7 +893,7 @@ let vernac_end_module export {loc;v=id} =
Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mty_ast_l with
@@ -969,7 +969,7 @@ let warn_require_in_section =
(fun () -> strbrk "Use of “Require” inside a section is deprecated.")
let vernac_require from import qidl =
- if Lib.sections_are_opened () then warn_require_in_section ();
+ if Global.sections_are_opened () then warn_require_in_section ();
let root = match from with
| None -> None
| Some from ->
@@ -2098,7 +2098,7 @@ let vernac_register qid r =
| RegisterCoqlib n ->
let ns, id = Libnames.repr_qualid n in
if DirPath.equal (dirpath_of_string "kernel") ns then begin
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
user_err Pp.(str "Registering a kernel type is not allowed in sections");
let pind = match Id.to_string id with
| "ind_bool" -> CPrimitives.PIT_bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:45:41 +0000