diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 39 | ||||
| -rw-r--r-- | library/declaremods.ml | 6 | ||||
| -rw-r--r-- | library/declaremods.mli | 3 | ||||
| -rw-r--r-- | library/universes.ml | 3 | ||||
| -rw-r--r-- | library/universes.mli | 2 |
5 files changed, 43 insertions, 10 deletions
diff --git a/library/declare.ml b/library/declare.ml index b0df32b8de..84284fd182 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -440,8 +440,9 @@ let cache_universes (p, l) = let glob = Universes.global_universe_names () in let glob', ctx = List.fold_left (fun ((idl,lid),ctx) (id, lev) -> - ((Idmap.add id lev idl, Univ.LMap.add lev id lid), - Univ.ContextSet.add_universe lev ctx)) + ((Idmap.add id (p, lev) idl, + Univ.LMap.add lev id lid), + Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in Global.push_context_set p ctx; @@ -457,6 +458,12 @@ let input_universes : universe_decl -> Libobject.obj = classify_function = (fun a -> Keep a) } let do_universe poly l = + let in_section = Lib.sections_are_opened () in + let () = + if poly && not in_section then + user_err_loc (Loc.ghost, "Constraint", + str"Cannot declare polymorphic universes outside sections") + in let l = List.map (fun (l, id) -> let lev = Universes.new_univ_level (Global.current_dirpath ()) in @@ -485,14 +492,30 @@ let input_constraints : constraint_decl -> Libobject.obj = let do_constraint poly l = let u_of_id = let names, _ = Universes.global_universe_names () in - fun (loc, id) -> - try Idmap.find id names - with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + fun (loc, id) -> + try Idmap.find id names + with Not_found -> + user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + in + let in_section = Lib.sections_are_opened () in + let () = + if poly && not in_section then + user_err_loc (Loc.ghost, "Constraint", + str"Cannot declare polymorphic constraints outside sections") + in + let check_poly loc p loc' p' = + if poly then () + else if p || p' then + let loc = if p then loc else loc' in + user_err_loc (loc, "Constraint", + str "Cannot declare a global constraint on " ++ + str "a polymorphic universe, use " + ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let lu = u_of_id l and ru = u_of_id r in - Univ.Constraint.add (lu, d, ru) acc) + let p, lu = u_of_id l and p', ru = u_of_id r in + check_poly (fst l) p (fst r) p'; + Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in Lib.add_anonymous_leaf (input_constraints (poly, constraints)) diff --git a/library/declaremods.ml b/library/declaremods.ml index f3f734aa09..dcd63c7691 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -897,7 +897,13 @@ let start_library dir = Lib.start_compilation dir mp; Lib.add_frozen_state () +let end_library_hook = ref ignore +let append_end_library_hook f = + let old_f = !end_library_hook in + end_library_hook := fun () -> old_f(); f () + let end_library ?except dir = + !end_library_hook(); let oname = Lib.end_compilation_checks dir in let mp,cenv,ast = Global.export ?except dir in let prefix, lib_stack = Lib.end_compilation oname in diff --git a/library/declaremods.mli b/library/declaremods.mli index 2b440c087a..3917fe8d64 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -90,6 +90,9 @@ val end_library : ?except:Future.UUIDSet.t -> library_name -> Safe_typing.compiled_library * library_objects * Safe_typing.native_library +(** append a function to be executed at end_library *) +val append_end_library_hook : (unit -> unit) -> unit + (** [really_import_module mp] opens the module [mp] (in a Caml sense). It modifies Nametab and performs the [open_object] function for every object of the module. Raises [Not_found] when [mp] is unknown diff --git a/library/universes.ml b/library/universes.ml index c4eb2afcbb..75cbd5604b 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -13,10 +13,11 @@ open Term open Environ open Univ open Globnames +open Decl_kinds (** Global universe names *) type universe_names = - Univ.universe_level Idmap.t * Id.t Univ.LMap.t + (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t let global_universes = Summary.ref ~name:"Global universe names" diff --git a/library/universes.mli b/library/universes.mli index 53cf5f3844..a5740ec49f 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -19,7 +19,7 @@ val is_set_minimization : unit -> bool (** Global universe name <-> level mapping *) type universe_names = - Univ.universe_level Idmap.t * Id.t Univ.LMap.t + (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t val global_universe_names : unit -> universe_names val set_global_universe_names : universe_names -> unit |