diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 50 | ||||
| -rw-r--r-- | library/declare.mli | 8 | ||||
| -rw-r--r-- | library/lib.ml | 30 | ||||
| -rw-r--r-- | library/lib.mli | 9 | ||||
| -rw-r--r-- | library/loadpath.ml | 3 |
5 files changed, 43 insertions, 57 deletions
diff --git a/library/declare.ml b/library/declare.ml index 3d063225f4..c5b83c11a0 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -434,6 +434,23 @@ let assumption_message id = (** Global universe names, in a different summary *) +type universe_context_decl = polymorphic * Univ.universe_context_set + +let cache_universe_context (p, ctx) = + Global.push_context_set p ctx; + if p then Lib.add_section_context ctx + +let input_universe_context : universe_context_decl -> Libobject.obj = + declare_object + { (default_object "Global universe context state") with + cache_function = (fun (na, pi) -> cache_universe_context pi); + load_function = (fun _ (_, pi) -> cache_universe_context pi); + discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); + classify_function = (fun a -> Keep a) } + +let declare_universe_context poly ctx = + Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) + (* Discharged or not *) type universe_decl = polymorphic * (Id.t * Univ.universe_level) list @@ -446,9 +463,8 @@ let cache_universes (p, l) = Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in - Global.push_context_set p ctx; - if p then Lib.add_section_context ctx; - Universes.set_global_universe_names glob' + cache_universe_context (p, ctx); + Universes.set_global_universe_names glob' let input_universes : universe_decl -> Libobject.obj = declare_object @@ -475,8 +491,8 @@ let do_universe poly l = type constraint_decl = polymorphic * Univ.constraints let cache_constraints (na, (p, c)) = - Global.add_constraints c; - if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty) + let ctx = Univ.ContextSet.add_constraints c Univ.ContextSet.empty in + cache_universe_context (p,ctx) let discharge_constraints (_, (p, c as a)) = if p then None else Some a @@ -491,12 +507,20 @@ let input_constraints : constraint_decl -> Libobject.obj = classify_function = (fun a -> Keep a) } 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) + let open Misctypes in + let u_of_id x = + match x with + | GProp -> Loc.dummy_loc, (false, Univ.Level.prop) + | GSet -> Loc.dummy_loc, (false, Univ.Level.set) + | GType None -> + user_err_loc (Loc.dummy_loc, "Constraint", + str "Cannot declare constraints on anonymous universes") + | GType (Some (loc, id)) -> + let id = Id.of_string id in + let names, _ = Universes.global_universe_names () in + try loc, 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 () = @@ -514,8 +538,8 @@ let do_constraint poly l = ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let p, lu = u_of_id l and p', ru = u_of_id r in - check_poly (fst l) p (fst r) p'; + let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in + check_poly ploc p rloc p'; Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in diff --git a/library/declare.mli b/library/declare.mli index 7824506da0..f70d594d7e 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -87,7 +87,11 @@ val exists_name : Id.t -> bool -(** Global universe names and constraints *) +(** Global universe contexts, names and constraints *) + +val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit val do_universe : polymorphic -> Id.t Loc.located list -> unit -val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit +val do_constraint : polymorphic -> + (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> + unit diff --git a/library/lib.ml b/library/lib.ml index 8880a8b154..7218950da3 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -506,13 +506,6 @@ let section_instance = function let is_in_section ref = try ignore (section_instance ref); true with Not_found -> false -let full_replacement_context () = List.map pi2 !sectab -let full_section_segment_of_constant con = - List.map (fun (vars,_,(x,_)) -> fun hyps -> - named_of_variable_context - (try pi1 (Names.Cmap.find con x) - with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab - (*************) (* Sections. *) @@ -613,15 +606,6 @@ let rec dp_of_mp = function |Names.MPbound _ -> library_dp () |Names.MPdot (mp,_) -> dp_of_mp mp -let rec split_mp = function - |Names.MPfile dp -> dp, Names.DirPath.empty - |Names.MPdot (prfx, lbl) -> - let mprec, dprec = split_mp prfx in - mprec, Libnames.add_dirpath_suffix dprec (Names.Label.to_id lbl) - |Names.MPbound mbid -> - let (_,id,dp) = Names.MBId.repr mbid in - library_dp (), Names.DirPath.make [id] - let rec split_modpath = function |Names.MPfile dp -> dp, [] |Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid] @@ -633,20 +617,6 @@ let library_part = function |VarRef id -> library_dp () |ref -> dp_of_mp (mp_of_global ref) -let remove_section_part ref = - let sp = Nametab.path_of_global ref in - let dir,_ = repr_path sp in - match ref with - | VarRef id -> - anomaly (Pp.str "remove_section_part not supported on local variables") - | _ -> - if is_dirpath_prefix_of dir (cwd ()) then - (* Not yet (fully) discharged *) - pop_dirpath_n (sections_depth ()) (cwd ()) - else - (* Theorem/Lemma outside its outer section of definition *) - dir - (************************) (* Discharging names *) diff --git a/library/lib.mli b/library/lib.mli index 7080b5dba7..0a70152efb 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -138,10 +138,8 @@ val library_dp : unit -> Names.DirPath.t (** Extract the library part of a name even if in a section *) val dp_of_mp : Names.module_path -> Names.DirPath.t -val split_mp : Names.module_path -> Names.DirPath.t * Names.DirPath.t val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list val library_part : Globnames.global_reference -> Names.DirPath.t -val remove_section_part : Globnames.global_reference -> Names.DirPath.t (** {6 Sections } *) @@ -191,10 +189,3 @@ val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive - -(* discharging a constant in one go *) -val full_replacement_context : unit -> Opaqueproof.work_list list -val full_section_segment_of_constant : - Names.constant -> (Context.Named.t -> Context.Named.t) list - - diff --git a/library/loadpath.ml b/library/loadpath.ml index e6f6716c3d..d03c6c5553 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -72,9 +72,6 @@ let add_load_path phys_path coq_path ~implicit = let replace = if DirPath.equal coq_path old_path then implicit <> old_implicit - else if DirPath.equal coq_path (Nameops.default_root_prefix) - && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then - false (* This is the default "-I ." path, don't override the old path *) else let () = (* Do not warn when overriding the default "-I ." path *) |