aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml8
-rw-r--r--library/declare.ml6
-rw-r--r--library/declaremods.ml11
-rw-r--r--library/global.ml2
-rw-r--r--library/globnames.ml2
-rw-r--r--library/goptions.ml14
-rw-r--r--library/heads.ml3
-rw-r--r--library/impargs.ml8
-rw-r--r--library/kindops.ml4
-rw-r--r--library/lib.ml19
-rw-r--r--library/lib.mli5
-rw-r--r--library/library.ml2
-rw-r--r--library/loadpath.ml2
-rw-r--r--library/nametab.ml2
-rw-r--r--library/summary.ml6
15 files changed, 38 insertions, 56 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 955ff4c089..0cb8c7afcf 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -52,14 +52,14 @@ let gen_reference_in_modules locstr dirs s =
| [] ->
anomaly ~label:locstr (str "cannot find " ++ str s ++
str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
- prlist_with_sep pr_comma pr_dirpath dirs)
+ prlist_with_sep pr_comma pr_dirpath dirs ++ str ".")
| l ->
anomaly ~label:locstr
(str "ambiguous name " ++ str s ++ str " can represent " ++
prlist_with_sep pr_comma
(fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
- prlist_with_sep pr_comma pr_dirpath dirs)
+ prlist_with_sep pr_comma pr_dirpath dirs ++ str ".")
(* For tactics/commands requiring vernacular libraries *)
@@ -185,7 +185,7 @@ let build_bool_type () =
andb_prop = init_reference ["Datatypes"] "andb_prop";
andb_true_intro = init_reference ["Datatypes"] "andb_true_intro" }
-let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type")
+let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type.")
let build_sigma_type () =
{ proj1 = init_reference ["Specif"] "projT1";
@@ -368,7 +368,7 @@ let coq_eq_ref = lazy (init_reference ["Logic"] "eq")
let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
let coq_jmeq_ref = lazy (find_reference "Coqlib" [coq;"Logic";"JMeq"] "JMeq")
let coq_eq_true_ref = lazy (find_reference "Coqlib" [coq;"Init";"Datatypes"] "eq_true")
-let coq_existS_ref = lazy (anomaly (Pp.str "use coq_existT_ref"))
+let coq_existS_ref = lazy (anomaly (Pp.str "use coq_existT_ref."))
let coq_existT_ref = lazy (init_reference ["Specif"] "existT")
let coq_exist_ref = lazy (init_reference ["Specif"] "exist")
let coq_not_ref = lazy (init_reference ["Logic"] "not")
diff --git a/library/declare.ml b/library/declare.ml
index 95b3674c3e..7d0edbc8b3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -149,7 +149,7 @@ let cache_constant ((sp,kn), obj) =
obj.cst_was_seff <- false;
if Global.exists_objlabel (Label.of_id (basename sp))
then constant_of_kn kn
- else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
+ else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
end else
let () = check_exists sp in
let kn', exported = Global.add_constant dir id obj.cst_decl in
@@ -385,7 +385,7 @@ let declare_projections mind =
let declare_mind mie =
let id = match mie.mind_entry_inds with
| ind::_ -> ind.mind_entry_typename
- | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in
+ | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
let mind = Global.mind_of_delta_kn kn in
let isrecord,isprim = declare_projections mind in
@@ -400,7 +400,7 @@ let pr_rank i = pr_nth (i+1)
let fixpoint_message indexes l =
Flags.if_verbose Feedback.msg_info (match l with
- | [] -> anomaly (Pp.str "no recursive definition")
+ | [] -> anomaly (Pp.str "no recursive definition.")
| [id] -> pr_id id ++ str " is recursively defined" ++
(match indexes with
| Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 08c33b5c15..187b749b87 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -252,7 +252,7 @@ let in_modkeep : Lib.lib_objects -> obj =
let do_modtype i sp mp sobjs =
if Nametab.exists_modtype sp then
- anomaly (pr_path sp ++ str " already exists");
+ anomaly (pr_path sp ++ str " already exists.");
Nametab.push_modtype (Nametab.Until i) sp mp;
ModSubstObjs.set mp sobjs
@@ -589,7 +589,6 @@ let start_module interp_modast export id args res fs =
openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
let prefix = Lib.start_module export id mp fs in
Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
- Lib.add_frozen_state ();
if_xml (Hook.get f_xml_start_module) mp;
mp
@@ -629,7 +628,6 @@ let end_module () =
assert (eq_full_path (fst newoname) (fst oldoname));
assert (ModPath.equal (mp_of_kn (snd newoname)) mp);
- Lib.add_frozen_state () (* to prevent recaching *);
if_xml (Hook.get f_xml_end_module) mp;
mp
@@ -701,7 +699,6 @@ let start_modtype interp_modast id args mtys fs =
openmodtype_info := sub_mty_l;
let prefix = Lib.start_modtype id mp fs in
Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
- Lib.add_frozen_state ();
if_xml (Hook.get f_xml_start_module_type) mp;
mp
@@ -719,7 +716,6 @@ let end_modtype () =
assert (eq_full_path (fst oname) (fst oldoname));
assert (ModPath.equal (mp_of_kn (snd oname)) mp);
- Lib.add_frozen_state ()(* to prevent recaching *);
if_xml (Hook.get f_xml_end_module_type) mp;
mp
@@ -883,7 +879,7 @@ let register_library dir cenv (objs:library_objects) digest univ =
(* If not, let's do it now ... *)
let mp' = Global.import cenv univ digest in
if not (ModPath.equal mp mp') then
- anomaly (Pp.str "Unexpected disk module name");
+ anomaly (Pp.str "Unexpected disk module name.");
in
let sobjs,keepobjs = objs in
do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
@@ -894,8 +890,7 @@ let get_library_native_symbols dir =
let start_library dir =
let mp = Global.start_library dir in
openmod_info := default_module_info;
- Lib.start_compilation dir mp;
- Lib.add_frozen_state ()
+ Lib.start_compilation dir mp
let end_library_hook = ref ignore
let append_end_library_hook f =
diff --git a/library/global.ml b/library/global.ml
index 5fa710b360..1ba86699d3 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -44,7 +44,7 @@ let () =
let assert_not_parsing () =
if !Flags.we_are_parsing then
CErrors.anomaly (
- Pp.strbrk"The global environment cannot be accessed during parsing")
+ Pp.strbrk"The global environment cannot be accessed during parsing.")
let safe_env () = assert_not_parsing(); !global_env
diff --git a/library/globnames.ml b/library/globnames.ml
index a78f5f13a9..9aeb379737 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -242,4 +242,4 @@ let pop_global_reference = function
| ConstRef con -> ConstRef (pop_con con)
| IndRef (kn,i) -> IndRef (pop_kn kn,i)
| ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
- | VarRef id -> anomaly (Pp.str "VarRef not poppable")
+ | VarRef id -> anomaly (Pp.str "VarRef not poppable.")
diff --git a/library/goptions.ml b/library/goptions.ml
index a803771cbc..a305214e82 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -273,23 +273,23 @@ type 'a write_function = 'a -> unit
let declare_int_option =
declare_option
(fun v -> IntValue v)
- (function IntValue v -> v | _ -> anomaly (Pp.str "async_option"))
- (fun _ _ -> anomaly (Pp.str "async_option"))
+ (function IntValue v -> v | _ -> anomaly (Pp.str "async_option."))
+ (fun _ _ -> anomaly (Pp.str "async_option."))
let declare_bool_option =
declare_option
(fun v -> BoolValue v)
- (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option"))
- (fun _ _ -> anomaly (Pp.str "async_option"))
+ (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option."))
+ (fun _ _ -> anomaly (Pp.str "async_option."))
let declare_string_option =
declare_option
(fun v -> StringValue v)
- (function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
+ (function StringValue v -> v | _ -> anomaly (Pp.str "async_option."))
(fun x y -> x^","^y)
let declare_stringopt_option =
declare_option
(fun v -> StringOptValue v)
- (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option"))
- (fun _ _ -> anomaly (Pp.str "async_option"))
+ (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option."))
+ (fun _ _ -> anomaly (Pp.str "async_option."))
(* 3- User accessible commands *)
diff --git a/library/heads.ml b/library/heads.ml
index 02465f22fc..6aee63c744 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -72,7 +72,8 @@ let kind_of_head env t =
with Not_found ->
CErrors.anomaly
Pp.(str "constant not found in kind_of_head: " ++
- str (Names.Constant.to_string cst)))
+ Names.Constant.print cst ++
+ str "."))
| Construct _ | CoFix _ ->
if b then NotImmediatelyComputableHead else ConstructorHead
| Sort _ | Ind _ | Prod _ -> RigidHead RigidType
diff --git a/library/impargs.ml b/library/impargs.ml
index 885185da1a..8f3bfc17e4 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -291,16 +291,16 @@ let is_status_implicit = function
| _ -> true
let name_of_implicit = function
- | None -> anomaly (Pp.str "Not an implicit argument")
+ | None -> anomaly (Pp.str "Not an implicit argument.")
| Some (id,_,_) -> id
let maximal_insertion_of = function
| Some (_,_,(b,_)) -> b
- | None -> anomaly (Pp.str "Not an implicit argument")
+ | None -> anomaly (Pp.str "Not an implicit argument.")
let force_inference_of = function
| Some (_, _, (_, b)) -> b
- | None -> anomaly (Pp.str "Not an implicit argument")
+ | None -> anomaly (Pp.str "Not an implicit argument.")
(* [in_ctx] means we know the expected type, [n] is the index of the argument *)
let is_inferable_implicit in_ctx n = function
@@ -324,7 +324,7 @@ let positions_of_implicits (_,impls) =
let rec prepare_implicits f = function
| [] -> []
- | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit")
+ | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
| (Name id, Some imp)::imps ->
let imps' = prepare_implicits f imps in
Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
diff --git a/library/kindops.ml b/library/kindops.ml
index 21b1bec33c..623d2537aa 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -25,7 +25,7 @@ let string_of_theorem_kind = function
let string_of_definition_kind def =
let (locality, poly, kind) = def in
- let error () = CErrors.anomaly (Pp.str "Internal definition kind") in
+ let error () = CErrors.anomaly (Pp.str "Internal definition kind.") in
match kind with
| Definition ->
begin match locality with
@@ -64,4 +64,4 @@ let string_of_definition_kind def =
| Global -> "Global Instance"
end
| (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
- CErrors.anomaly (Pp.str "Internal definition kind")
+ CErrors.anomaly (Pp.str "Internal definition kind.")
diff --git a/library/lib.ml b/library/lib.ml
index 4ad4e261d7..f22f53eadf 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -27,7 +27,6 @@ type node =
| ClosedModule of library_segment
| OpenedSection of object_prefix * Summary.frozen
| ClosedSection of library_segment
- | FrozenState of Summary.frozen
and library_entry = object_name * node
@@ -80,7 +79,6 @@ let classify_segment seg =
| (_,OpenedModule (ty,_,_,_)) :: _ ->
user_err ~hdr:"Lib.classify_segment"
(str "there are still opened " ++ str (module_kind ty) ++ str "s")
- | (_,FrozenState _) :: stk -> clean acc stk
in
clean ([],[],[]) (List.rev seg)
@@ -254,10 +252,6 @@ let add_anonymous_leaf ?(cache_first = true) obj =
cache_object (oname,obj)
end
-let add_frozen_state () =
- add_anonymous_entry
- (FrozenState (Summary.freeze_summaries ~marshallable:`No))
-
(* Modules. *)
let is_opening_node = function
@@ -350,7 +344,7 @@ let end_compilation_checks dir =
try match find_entry_p is_opening_lib with
| (oname, CompilingLibrary prefix) -> oname
| _ -> assert false
- with Not_found -> anomaly (Pp.str "No module declared")
+ with Not_found -> anomaly (Pp.str "No module declared.")
in
let _ =
match !lib_state.comp_name with
@@ -358,7 +352,7 @@ let end_compilation_checks dir =
| Some m ->
if not (Names.DirPath.equal m dir) then anomaly
(str "The current open module has name" ++ spc () ++ pr_dirpath m ++
- spc () ++ str "and not" ++ spc () ++ pr_dirpath m);
+ spc () ++ str "and not" ++ spc () ++ pr_dirpath m ++ str ".");
in
oname
@@ -544,10 +538,9 @@ let discharge_item ((sp,_ as oname),e) =
match e with
| Leaf lobj ->
Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
- | FrozenState _ -> None
| ClosedSection _ | ClosedModule _ -> None
| OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
- anomaly (Pp.str "discharge_item")
+ anomaly (Pp.str "discharge_item.")
let close_section () =
let oname,fs =
@@ -585,8 +578,7 @@ let freeze ~marshallable =
| n, ClosedModule _ -> Some (n,ClosedModule [])
| n, OpenedSection (op, _) ->
Some(n,OpenedSection(op,Summary.empty_frozen))
- | n, ClosedSection _ -> Some (n,ClosedSection [])
- | _, FrozenState _ -> None)
+ | n, ClosedSection _ -> Some (n,ClosedSection []))
!lib_state.lib_stk in
{ !lib_state with lib_stk }
| _ ->
@@ -596,8 +588,7 @@ let unfreeze st = lib_state := st
let init () =
unfreeze initial_lib_state;
- Summary.init_summaries ();
- add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *)
+ Summary.init_summaries ()
(* Misc *)
diff --git a/library/lib.mli b/library/lib.mli
index 9f9d8c7e5f..f47d6e1a58 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -23,7 +23,6 @@ type node =
| ClosedModule of library_segment
| OpenedSection of Libnames.object_prefix * Summary.frozen
| ClosedSection of library_segment
- | FrozenState of Summary.frozen
and library_segment = (Libnames.object_name * node) list
@@ -61,8 +60,6 @@ val pull_to_head : Libnames.object_name -> unit
for each of them *)
val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name
-val add_frozen_state : unit -> unit
-
(** {6 ... } *)
(** The function [contents] gives access to the current entire segment *)
@@ -123,8 +120,6 @@ val end_modtype :
Libnames.object_name * Libnames.object_prefix *
Summary.frozen * library_segment
-(** [Lib.add_frozen_state] must be called after each of the above functions *)
-
(** {6 Compilation units } *)
val start_compilation : Names.DirPath.t -> Names.module_path -> unit
diff --git a/library/library.ml b/library/library.ml
index 5a5f99cc51..db05ad2b7b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -575,7 +575,7 @@ let require_library_from_dirpath modrefl export =
else
add_anonymous_leaf (in_require (needed,modrefl,export));
if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl;
- add_frozen_state ()
+ ()
(* the function called by Vernacentries.vernac_import *)
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 529b9502b0..ad429ea840 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -29,7 +29,7 @@ let physical p = p.path_physical
let get_load_paths () = !load_paths
let anomaly_too_many_paths path =
- anomaly (str "Several logical paths are associated to" ++ spc () ++ str path)
+ anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".")
let find_load_path phys_dir =
let phys_dir = CUnix.canonical_path_name phys_dir in
diff --git a/library/nametab.ml b/library/nametab.ml
index 2e4e98013e..93e9c03cee 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -294,7 +294,7 @@ module DirPath' =
struct
include DirPath
let repr dir = match DirPath.repr dir with
- | [] -> anomaly (Pp.str "Empty dirpath")
+ | [] -> anomaly (Pp.str "Empty dirpath.")
| id :: l -> (id, l)
end
diff --git a/library/summary.ml b/library/summary.ml
index d9f6441003..c7bf95fd41 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -46,7 +46,7 @@ let declare_summary sumname decl =
let () = if Int.Map.mem hash !summaries then
let (name, _) = Int.Map.find hash !summaries in
anomaly ~label:"Summary.declare_summary"
- (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name)
+ (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name ++ str ".")
in
all_declared_summaries := Int.Set.add hash !all_declared_summaries;
summary_names := (hash, sumname) :: !summary_names;
@@ -85,10 +85,10 @@ let unfreeze_summaries fs =
* may modify the content of [summaries] ny loading new ML modules *)
let (_, decl) =
try Int.Map.find ml_modules_summary !summaries
- with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules)
+ with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
in
let () = match fs.ml_module with
- | None -> anomaly (str "Undeclared summary " ++ str ml_modules)
+ | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
| Some state -> decl.unfreeze_function state
in
let fold id (_, decl) states =
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 07:37:17 +0000