aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml383
-rw-r--r--library/coqlib.mli211
-rw-r--r--library/declare.ml6
-rw-r--r--library/declaremods.ml10
-rw-r--r--library/global.ml2
-rw-r--r--library/globnames.ml2
-rw-r--r--library/goptions.ml22
-rw-r--r--library/heads.ml3
-rw-r--r--library/impargs.ml12
-rw-r--r--library/kindops.ml4
-rw-r--r--library/lib.ml30
-rw-r--r--library/libnames.ml4
-rw-r--r--library/library.ml2
-rw-r--r--library/library.mllib1
-rw-r--r--library/loadpath.ml2
-rw-r--r--library/nameops.ml97
-rw-r--r--library/nameops.mli61
-rw-r--r--library/nametab.ml6
-rw-r--r--library/summary.ml6
19 files changed, 777 insertions, 87 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
new file mode 100644
index 0000000000..0cb8c7afcf
--- /dev/null
+++ b/library/coqlib.ml
@@ -0,0 +1,383 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open CErrors
+open Util
+open Pp
+open Names
+open Libnames
+open Globnames
+open Nametab
+
+let coq = Nameops.coq_string (* "Coq" *)
+
+(************************************************************************)
+(* Generic functions to find Coq objects *)
+
+type message = string
+
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+
+let find_reference locstr dir s =
+ let dp = make_dir dir in
+ let sp = Libnames.make_path dp (Id.of_string s) in
+ try Nametab.global_of_path sp
+ with Not_found ->
+ (* Following bug 5066 we are more permissive with the handling
+ of not found errors here *)
+ user_err ~hdr:locstr
+ Pp.(str "cannot find " ++ Libnames.pr_path sp ++
+ str "; maybe library " ++ Libnames.pr_dirpath dp ++
+ str " has to be required first.")
+
+let coq_reference locstr dir s = find_reference locstr (coq::dir) s
+
+let has_suffix_in_dirs dirs ref =
+ let dir = dirpath (path_of_global ref) in
+ List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
+
+let gen_reference_in_modules locstr dirs s =
+ let dirs = List.map make_dir dirs in
+ let qualid = qualid_of_string s in
+ let all = Nametab.locate_all qualid in
+ let all = List.sort_uniquize RefOrdered_env.compare all in
+ let these = List.filter (has_suffix_in_dirs dirs) all in
+ match these with
+ | [x] -> x
+ | [] ->
+ 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 ++ 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 ++ str ".")
+
+(* For tactics/commands requiring vernacular libraries *)
+
+let check_required_library d =
+ let dir = make_dir d in
+ if Library.library_is_loaded dir then ()
+ else
+ let in_current_dir = match Lib.current_mp () with
+ | MPfile dp -> DirPath.equal dir dp
+ | _ -> false
+ in
+ if not in_current_dir then
+(* Loading silently ...
+ let m, prefix = List.sep_last d' in
+ read_library
+ (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m)
+*)
+(* or failing ...*)
+ user_err ~hdr:"Coqlib.check_required_library"
+ (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
+
+(************************************************************************)
+(* Specific Coq objects *)
+
+let init_reference dir s =
+ let d = coq::"Init"::dir in
+ check_required_library d; find_reference "Coqlib" d s
+
+let logic_reference dir s =
+ let d = coq::"Logic"::dir in
+ check_required_library d; find_reference "Coqlib" d s
+
+let arith_dir = [coq;"Arith"]
+let arith_modules = [arith_dir]
+
+let numbers_dir = [coq;"Numbers"]
+let parith_dir = [coq;"PArith"]
+let narith_dir = [coq;"NArith"]
+let zarith_dir = [coq;"ZArith"]
+
+let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir]
+
+let init_dir = [coq;"Init"]
+let init_modules = [
+ init_dir@["Datatypes"];
+ init_dir@["Logic"];
+ init_dir@["Specif"];
+ init_dir@["Logic_Type"];
+ init_dir@["Nat"];
+ init_dir@["Peano"];
+ init_dir@["Wf"]
+]
+
+let prelude_module_name = init_dir@["Prelude"]
+let prelude_module = make_dir prelude_module_name
+
+let logic_module_name = init_dir@["Logic"]
+let logic_module = make_dir logic_module_name
+
+let logic_type_module_name = init_dir@["Logic_Type"]
+let logic_type_module = make_dir logic_type_module_name
+
+let datatypes_module_name = init_dir@["Datatypes"]
+let datatypes_module = make_dir datatypes_module_name
+
+let jmeq_module_name = [coq;"Logic";"JMeq"]
+let jmeq_module = make_dir jmeq_module_name
+
+(* TODO: temporary hack. Works only if the module isn't an alias *)
+let make_ind dir id = Globnames.encode_mind dir (Id.of_string id)
+let make_con dir id = Globnames.encode_con dir (Id.of_string id)
+
+(** Identity *)
+
+let id = make_con datatypes_module "idProp"
+let type_of_id = make_con datatypes_module "IDProp"
+
+(** Natural numbers *)
+let nat_kn = make_ind datatypes_module "nat"
+let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat")
+
+let glob_nat = IndRef (nat_kn,0)
+
+let path_of_O = ((nat_kn,0),1)
+let path_of_S = ((nat_kn,0),2)
+let glob_O = ConstructRef path_of_O
+let glob_S = ConstructRef path_of_S
+
+(** Booleans *)
+let bool_kn = make_ind datatypes_module "bool"
+
+let glob_bool = IndRef (bool_kn,0)
+
+let path_of_true = ((bool_kn,0),1)
+let path_of_false = ((bool_kn,0),2)
+let glob_true = ConstructRef path_of_true
+let glob_false = ConstructRef path_of_false
+
+(** Equality *)
+let eq_kn = make_ind logic_module "eq"
+let glob_eq = IndRef (eq_kn,0)
+
+let identity_kn = make_ind datatypes_module "identity"
+let glob_identity = IndRef (identity_kn,0)
+
+let jmeq_kn = make_ind jmeq_module "JMeq"
+let glob_jmeq = IndRef (jmeq_kn,0)
+
+type coq_sigma_data = {
+ proj1 : global_reference;
+ proj2 : global_reference;
+ elim : global_reference;
+ intro : global_reference;
+ typ : global_reference }
+
+type coq_bool_data = {
+ andb : global_reference;
+ andb_prop : global_reference;
+ andb_true_intro : global_reference}
+
+let build_bool_type () =
+ { andb = init_reference ["Datatypes"] "andb";
+ 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_type () =
+ { proj1 = init_reference ["Specif"] "projT1";
+ proj2 = init_reference ["Specif"] "projT2";
+ elim = init_reference ["Specif"] "sigT_rect";
+ intro = init_reference ["Specif"] "existT";
+ typ = init_reference ["Specif"] "sigT" }
+
+let build_sigma () =
+ { proj1 = init_reference ["Specif"] "proj1_sig";
+ proj2 = init_reference ["Specif"] "proj2_sig";
+ elim = init_reference ["Specif"] "sig_rect";
+ intro = init_reference ["Specif"] "exist";
+ typ = init_reference ["Specif"] "sig" }
+
+
+let build_prod () =
+ { proj1 = init_reference ["Datatypes"] "fst";
+ proj2 = init_reference ["Datatypes"] "snd";
+ elim = init_reference ["Datatypes"] "prod_rec";
+ intro = init_reference ["Datatypes"] "pair";
+ typ = init_reference ["Datatypes"] "prod" }
+
+(* Equalities *)
+type coq_eq_data = {
+ eq : global_reference;
+ ind : global_reference;
+ refl : global_reference;
+ sym : global_reference;
+ trans: global_reference;
+ congr: global_reference }
+
+(* Data needed for discriminate and injection *)
+type coq_inversion_data = {
+ inv_eq : global_reference; (* : forall params, t -> Prop *)
+ inv_ind : global_reference; (* : forall params P y, eq params y -> P y *)
+ inv_congr: global_reference (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
+}
+
+let lazy_init_reference dir id = lazy (init_reference dir id)
+let lazy_logic_reference dir id = lazy (logic_reference dir id)
+
+(* Leibniz equality on Type *)
+
+let coq_eq_eq = lazy_init_reference ["Logic"] "eq"
+let coq_eq_refl = lazy_init_reference ["Logic"] "eq_refl"
+let coq_eq_ind = lazy_init_reference ["Logic"] "eq_ind"
+let coq_eq_congr = lazy_init_reference ["Logic"] "f_equal"
+let coq_eq_sym = lazy_init_reference ["Logic"] "eq_sym"
+let coq_eq_trans = lazy_init_reference ["Logic"] "eq_trans"
+let coq_f_equal2 = lazy_init_reference ["Logic"] "f_equal2"
+let coq_eq_congr_canonical =
+ lazy_init_reference ["Logic"] "f_equal_canonical_form"
+
+let build_coq_eq_data () =
+ let _ = check_required_library logic_module_name in {
+ eq = Lazy.force coq_eq_eq;
+ ind = Lazy.force coq_eq_ind;
+ refl = Lazy.force coq_eq_refl;
+ sym = Lazy.force coq_eq_sym;
+ trans = Lazy.force coq_eq_trans;
+ congr = Lazy.force coq_eq_congr }
+
+let build_coq_eq () = Lazy.force coq_eq_eq
+let build_coq_eq_refl () = Lazy.force coq_eq_refl
+let build_coq_eq_sym () = Lazy.force coq_eq_sym
+let build_coq_f_equal2 () = Lazy.force coq_f_equal2
+
+let build_coq_inversion_eq_data () =
+ let _ = check_required_library logic_module_name in {
+ inv_eq = Lazy.force coq_eq_eq;
+ inv_ind = Lazy.force coq_eq_ind;
+ inv_congr = Lazy.force coq_eq_congr_canonical }
+
+(* Heterogenous equality on Type *)
+
+let coq_jmeq_eq = lazy_logic_reference ["JMeq"] "JMeq"
+let coq_jmeq_hom = lazy_logic_reference ["JMeq"] "JMeq_hom"
+let coq_jmeq_refl = lazy_logic_reference ["JMeq"] "JMeq_refl"
+let coq_jmeq_ind = lazy_logic_reference ["JMeq"] "JMeq_ind"
+let coq_jmeq_sym = lazy_logic_reference ["JMeq"] "JMeq_sym"
+let coq_jmeq_congr = lazy_logic_reference ["JMeq"] "JMeq_congr"
+let coq_jmeq_trans = lazy_logic_reference ["JMeq"] "JMeq_trans"
+let coq_jmeq_congr_canonical =
+ lazy_logic_reference ["JMeq"] "JMeq_congr_canonical_form"
+
+let build_coq_jmeq_data () =
+ let _ = check_required_library jmeq_module_name in {
+ eq = Lazy.force coq_jmeq_eq;
+ ind = Lazy.force coq_jmeq_ind;
+ refl = Lazy.force coq_jmeq_refl;
+ sym = Lazy.force coq_jmeq_sym;
+ trans = Lazy.force coq_jmeq_trans;
+ congr = Lazy.force coq_jmeq_congr }
+
+let build_coq_inversion_jmeq_data () =
+ let _ = check_required_library logic_module_name in {
+ inv_eq = Lazy.force coq_jmeq_hom;
+ inv_ind = Lazy.force coq_jmeq_ind;
+ inv_congr = Lazy.force coq_jmeq_congr_canonical }
+
+(* Specif *)
+let coq_sumbool = lazy_init_reference ["Specif"] "sumbool"
+
+let build_coq_sumbool () = Lazy.force coq_sumbool
+
+(* Equality on Type as a Type *)
+let coq_identity_eq = lazy_init_reference ["Datatypes"] "identity"
+let coq_identity_refl = lazy_init_reference ["Datatypes"] "identity_refl"
+let coq_identity_ind = lazy_init_reference ["Datatypes"] "identity_ind"
+let coq_identity_congr = lazy_init_reference ["Logic_Type"] "identity_congr"
+let coq_identity_sym = lazy_init_reference ["Logic_Type"] "identity_sym"
+let coq_identity_trans = lazy_init_reference ["Logic_Type"] "identity_trans"
+let coq_identity_congr_canonical = lazy_init_reference ["Logic_Type"] "identity_congr_canonical_form"
+
+let build_coq_identity_data () =
+ let _ = check_required_library datatypes_module_name in {
+ eq = Lazy.force coq_identity_eq;
+ ind = Lazy.force coq_identity_ind;
+ refl = Lazy.force coq_identity_refl;
+ sym = Lazy.force coq_identity_sym;
+ trans = Lazy.force coq_identity_trans;
+ congr = Lazy.force coq_identity_congr }
+
+let build_coq_inversion_identity_data () =
+ let _ = check_required_library datatypes_module_name in
+ let _ = check_required_library logic_type_module_name in {
+ inv_eq = Lazy.force coq_identity_eq;
+ inv_ind = Lazy.force coq_identity_ind;
+ inv_congr = Lazy.force coq_identity_congr_canonical }
+
+(* Equality to true *)
+let coq_eq_true_eq = lazy_init_reference ["Datatypes"] "eq_true"
+let coq_eq_true_ind = lazy_init_reference ["Datatypes"] "eq_true_ind"
+let coq_eq_true_congr = lazy_init_reference ["Logic"] "eq_true_congr"
+
+let build_coq_inversion_eq_true_data () =
+ let _ = check_required_library datatypes_module_name in
+ let _ = check_required_library logic_module_name in {
+ inv_eq = Lazy.force coq_eq_true_eq;
+ inv_ind = Lazy.force coq_eq_true_ind;
+ inv_congr = Lazy.force coq_eq_true_congr }
+
+(* The False proposition *)
+let coq_False = lazy_init_reference ["Logic"] "False"
+
+(* The True proposition and its unique proof *)
+let coq_True = lazy_init_reference ["Logic"] "True"
+let coq_I = lazy_init_reference ["Logic"] "I"
+
+(* Connectives *)
+let coq_not = lazy_init_reference ["Logic"] "not"
+let coq_and = lazy_init_reference ["Logic"] "and"
+let coq_conj = lazy_init_reference ["Logic"] "conj"
+let coq_or = lazy_init_reference ["Logic"] "or"
+let coq_ex = lazy_init_reference ["Logic"] "ex"
+let coq_iff = lazy_init_reference ["Logic"] "iff"
+
+let coq_iff_left_proj = lazy_init_reference ["Logic"] "proj1"
+let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2"
+
+(* Runtime part *)
+let build_coq_True () = Lazy.force coq_True
+let build_coq_I () = Lazy.force coq_I
+
+let build_coq_False () = Lazy.force coq_False
+let build_coq_not () = Lazy.force coq_not
+let build_coq_and () = Lazy.force coq_and
+let build_coq_conj () = Lazy.force coq_conj
+let build_coq_or () = Lazy.force coq_or
+let build_coq_ex () = Lazy.force coq_ex
+let build_coq_iff () = Lazy.force coq_iff
+
+let build_coq_iff_left_proj () = Lazy.force coq_iff_left_proj
+let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
+
+
+(* The following is less readable but does not depend on parsing *)
+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_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")
+let coq_False_ref = lazy (init_reference ["Logic"] "False")
+let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
+let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
+let coq_or_ref = lazy (init_reference ["Logic"] "or")
+let coq_iff_ref = lazy (init_reference ["Logic"] "iff")
+
+(* Deprecated *)
+let gen_reference = coq_reference
+
diff --git a/library/coqlib.mli b/library/coqlib.mli
new file mode 100644
index 0000000000..716d97c9d0
--- /dev/null
+++ b/library/coqlib.mli
@@ -0,0 +1,211 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Libnames
+open Globnames
+open Util
+
+(** This module collects the global references, constructions and
+ patterns of the standard library used in ocaml files *)
+
+(** The idea is to migrate to rebindable name-based approach, thus the
+ only function this FILE will provide will be:
+
+ [find_reference : string -> global_reference]
+
+ such that [find_reference "core.eq.type"] returns the proper [global_reference]
+
+ [bind_reference : string -> global_reference -> unit]
+
+ will bind a reference.
+
+ A feature based approach would be possible too.
+
+ Contrary to the old approach of raising an anomaly, we expect
+ tactics to gracefully fail in the absence of some primitive.
+
+ This is work in progress, see below.
+*)
+
+(** {6 ... } *)
+(** [find_reference caller_message [dir;subdir;...] s] returns a global
+ reference to the name dir.subdir.(...).s; the corresponding module
+ must have been required or in the process of being compiled so that
+ it must be used lazily; it raises an anomaly with the given message
+ if not found *)
+
+type message = string
+
+val find_reference : message -> string list -> string -> global_reference
+val coq_reference : message -> string list -> string -> global_reference
+
+(** For tactics/commands requiring vernacular libraries *)
+val check_required_library : string list -> unit
+
+(** Search in several modules (not prefixed by "Coq") *)
+val gen_reference_in_modules : string->string list list-> string -> global_reference
+
+val arith_modules : string list list
+val zarith_base_modules : string list list
+val init_modules : string list list
+
+(** {6 Global references } *)
+
+(** Modules *)
+val prelude_module : DirPath.t
+
+val logic_module : DirPath.t
+val logic_module_name : string list
+
+val logic_type_module : DirPath.t
+
+val jmeq_module : DirPath.t
+val jmeq_module_name : string list
+
+val datatypes_module_name : string list
+
+(** Identity *)
+val id : constant
+val type_of_id : constant
+
+(** Natural numbers *)
+val nat_path : full_path
+val glob_nat : global_reference
+val path_of_O : constructor
+val path_of_S : constructor
+val glob_O : global_reference
+val glob_S : global_reference
+
+(** Booleans *)
+val glob_bool : global_reference
+val path_of_true : constructor
+val path_of_false : constructor
+val glob_true : global_reference
+val glob_false : global_reference
+
+
+(** Equality *)
+val glob_eq : global_reference
+val glob_identity : global_reference
+val glob_jmeq : global_reference
+
+(** {6 ... } *)
+(** Constructions and patterns related to Coq initial state are unknown
+ at compile time. Therefore, we can only provide methods to build
+ them at runtime. This is the purpose of the [constr delayed] and
+ [constr_pattern delayed] types. Objects of this time needs to be
+ forced with [delayed_force] to get the actual constr or pattern
+ at runtime. *)
+
+type coq_bool_data = {
+ andb : global_reference;
+ andb_prop : global_reference;
+ andb_true_intro : global_reference}
+val build_bool_type : coq_bool_data delayed
+
+(** {6 For Equality tactics } *)
+type coq_sigma_data = {
+ proj1 : global_reference;
+ proj2 : global_reference;
+ elim : global_reference;
+ intro : global_reference;
+ typ : global_reference }
+
+val build_sigma_set : coq_sigma_data delayed
+val build_sigma_type : coq_sigma_data delayed
+val build_sigma : coq_sigma_data delayed
+
+(* val build_sigma_type_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *)
+(* val build_sigma_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *)
+(* val build_prod_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *)
+(* val build_coq_eq_data_in : Environ.env -> coq_eq_data Univ.in_universe_context_set *)
+
+(** Non-dependent pairs in Set from Datatypes *)
+val build_prod : coq_sigma_data delayed
+
+type coq_eq_data = {
+ eq : global_reference;
+ ind : global_reference;
+ refl : global_reference;
+ sym : global_reference;
+ trans: global_reference;
+ congr: global_reference }
+
+val build_coq_eq_data : coq_eq_data delayed
+
+val build_coq_identity_data : coq_eq_data delayed
+val build_coq_jmeq_data : coq_eq_data delayed
+
+val build_coq_eq : global_reference delayed (** = [(build_coq_eq_data()).eq] *)
+val build_coq_eq_refl : global_reference delayed (** = [(build_coq_eq_data()).refl] *)
+val build_coq_eq_sym : global_reference delayed (** = [(build_coq_eq_data()).sym] *)
+val build_coq_f_equal2 : global_reference delayed
+
+(** Data needed for discriminate and injection *)
+
+type coq_inversion_data = {
+ inv_eq : global_reference; (** : forall params, args -> Prop *)
+ inv_ind : global_reference; (** : forall params P (H : P params) args, eq params args
+ -> P args *)
+ inv_congr: global_reference (** : forall params B (f:t->B) args, eq params args ->
+ f params = f args *)
+}
+
+val build_coq_inversion_eq_data : coq_inversion_data delayed
+val build_coq_inversion_identity_data : coq_inversion_data delayed
+val build_coq_inversion_jmeq_data : coq_inversion_data delayed
+val build_coq_inversion_eq_true_data : coq_inversion_data delayed
+
+(** Specif *)
+val build_coq_sumbool : global_reference delayed
+
+(** {6 ... } *)
+(** Connectives
+ The False proposition *)
+val build_coq_False : global_reference delayed
+
+(** The True proposition and its unique proof *)
+val build_coq_True : global_reference delayed
+val build_coq_I : global_reference delayed
+
+(** Negation *)
+val build_coq_not : global_reference delayed
+
+(** Conjunction *)
+val build_coq_and : global_reference delayed
+val build_coq_conj : global_reference delayed
+val build_coq_iff : global_reference delayed
+
+val build_coq_iff_left_proj : global_reference delayed
+val build_coq_iff_right_proj : global_reference delayed
+
+(** Disjunction *)
+val build_coq_or : global_reference delayed
+
+(** Existential quantifier *)
+val build_coq_ex : global_reference delayed
+
+val coq_eq_ref : global_reference lazy_t
+val coq_identity_ref : global_reference lazy_t
+val coq_jmeq_ref : global_reference lazy_t
+val coq_eq_true_ref : global_reference lazy_t
+val coq_existS_ref : global_reference lazy_t
+val coq_existT_ref : global_reference lazy_t
+val coq_exist_ref : global_reference lazy_t
+val coq_not_ref : global_reference lazy_t
+val coq_False_ref : global_reference lazy_t
+val coq_sumbool_ref : global_reference lazy_t
+val coq_sig_ref : global_reference lazy_t
+
+val coq_or_ref : global_reference lazy_t
+val coq_iff_ref : global_reference lazy_t
+
+(* Deprecated functions *)
+val gen_reference : message -> string list -> string -> global_reference
+[@@ocaml.deprecated "Please use Coqlib.find_reference"]
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 3a263b1e12..c98d4a7f31 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
@@ -345,7 +345,7 @@ let get_applications mexpr =
let rec get params = function
| MEident mp -> mp, params
| MEapply (fexpr, mp) -> get (mp::params) fexpr
- | MEwith _ -> error "Non-atomic functor application."
+ | MEwith _ -> user_err Pp.(str "Non-atomic functor application.")
in get [] mexpr
(** Create the substitution corresponding to some functor applications *)
@@ -353,7 +353,7 @@ let get_applications mexpr =
let rec compute_subst env mbids sign mp_l inl =
match mbids,mp_l with
| _,[] -> mbids,empty_subst
- | [],r -> error "Application of a functor with too few arguments."
+ | [],r -> user_err Pp.(str "Application of a functor with too few arguments.")
| mbid::mbids,mp::mp_l ->
let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
let mb = Environ.lookup_module mp env in
@@ -777,7 +777,7 @@ let rec decompose_functor mpl typ =
match mpl, typ with
| [], _ -> typ
| _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str
- | _ -> error "Application of a functor with too much arguments."
+ | _ -> user_err Pp.(str "Application of a functor with too much arguments.")
exception NoIncludeSelf
@@ -883,7 +883,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
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 9b4fc99857..a305214e82 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -71,7 +71,7 @@ module MakeTable =
let _ =
if String.List.mem_assoc nick !A.table then
- error "Sorry, this table name is already used."
+ user_err Pp.(str "Sorry, this table name is already used.")
module MySet = Set.Make (struct type t = A.t let compare = A.compare end)
@@ -214,11 +214,11 @@ let get_option key = OptionMap.find key !value_tab
let check_key key = try
let _ = get_option key in
- error "Sorry, this option name is already used."
+ user_err Pp.(str "Sorry, this option name is already used.")
with Not_found ->
if String.List.mem_assoc (nickname key) !string_table
|| String.List.mem_assoc (nickname key) !ref_table
- then error "Sorry, this option name is already used."
+ then user_err Pp.(str "Sorry, this option name is already used.")
open Libobject
@@ -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 *)
@@ -307,7 +307,7 @@ let set_option_value locality check_and_cast key v =
| Some (name, depr, (read,write,append)) ->
write (get_locality locality) (check_and_cast v (read ()))
-let bad_type_error () = error "Bad type of value for this option."
+let bad_type_error () = user_err Pp.(str "Bad type of value for this option.")
let check_int_value v = function
| IntValue _ -> IntValue v
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 a63264b669..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'
@@ -364,7 +364,7 @@ let set_manual_implicits env flags enriching autoimps l =
with Not_found -> l, None
in
if not (List.distinct l) then
- error ("Some parameters are referred more than once.");
+ user_err Pp.(str "Some parameters are referred more than once.");
(* Compare with automatic implicits to recover printing data and names *)
let rec merge k l = function
| (Name id,imp)::imps ->
@@ -658,7 +658,7 @@ let check_inclusion l =
let rec aux = function
| n1::(n2::_ as nl) ->
if n1 <= n2 then
- error "Sequences of implicit arguments must be of different lengths.";
+ user_err Pp.(str "Sequences of implicit arguments must be of different lengths.");
aux nl
| _ -> () in
aux (List.map (fun (imps,_) -> List.length imps) l)
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 ddd2ed6afa..9d71a854f0 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -76,7 +76,7 @@ let classify_segment seg =
(* LEM; TODO: Understand what this does and see if what I do is the
correct thing for ClosedMod(ule|type) *)
| (_,ClosedModule _) :: stk -> clean acc stk
- | (_,OpenedSection _) :: _ -> error "there are still opened sections"
+ | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections")
| (_,OpenedModule (ty,_,_,_)) :: _ ->
user_err ~hdr:"Lib.classify_segment"
(str "there are still opened " ++ str (module_kind ty) ++ str "s")
@@ -184,7 +184,7 @@ let split_lib_gen test =
| [] -> None
in
match findeq [] !lib_state.lib_stk with
- | None -> error "no such entry"
+ | None -> user_err Pp.(str "no such entry")
| Some r -> r
let eq_object_name (fp1, kn1) (fp2, kn2) =
@@ -222,7 +222,7 @@ let add_anonymous_entry node =
let add_leaf id obj =
if Names.ModPath.equal (current_mp ()) Names.initial_path then
- error ("No session module started (use -top dir)");
+ user_err Pp.(str "No session module started (use -top dir)");
let oname = make_oname id in
cache_object (oname,obj);
add_entry oname (Leaf obj);
@@ -272,8 +272,8 @@ let current_mod_id () =
try match find_entry_p is_opening_node_or_lib with
| oname,OpenedModule (_,_,_,fs) -> basename (fst oname)
| oname,CompilingLibrary _ -> basename (fst oname)
- | _ -> error "you are not in a module"
- with Not_found -> error "no opened modules"
+ | _ -> user_err Pp.(str "you are not in a module")
+ with Not_found -> user_err Pp.(str "no opened modules")
let start_mod is_type export id mp fs =
@@ -305,7 +305,7 @@ let end_mod is_type =
else error_still_opened (module_kind ty) oname
| oname,OpenedSection _ -> error_still_opened "section" oname
| _ -> assert false
- with Not_found -> error "No opened modules."
+ with Not_found -> user_err (Pp.str "No opened modules.")
in
let (after,mark,before) = split_lib_at_opening oname in
lib_state := { !lib_state with lib_stk = before };
@@ -326,9 +326,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
(* TODO: use check_for_module ? *)
let start_compilation s mp =
if !lib_state.comp_name != None then
- error "compilation unit is already started";
+ user_err Pp.(str "compilation unit is already started");
if not (Names.DirPath.is_empty (current_sections ())) then
- error "some sections are already opened";
+ user_err Pp.(str "some sections are already opened");
let prefix = s, (mp, Names.DirPath.empty) in
let () = add_anonymous_entry (CompilingLibrary prefix) in
lib_state := { !lib_state with comp_name = Some s;
@@ -337,7 +337,7 @@ let start_compilation s mp =
let end_compilation_checks dir =
let _ =
try match snd (find_entry_p is_opening_node) with
- | OpenedSection _ -> error "There are some open sections."
+ | OpenedSection _ -> user_err Pp.(str "There are some open sections.")
| OpenedModule (ty,_,_,_) ->
user_err ~hdr:"Lib.end_compilation_checks"
(str "There are some open " ++ str (module_kind ty) ++ str "s.")
@@ -350,7 +350,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 +358,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
@@ -394,7 +394,7 @@ let find_opening_node id =
user_err ~hdr:"Lib.find_opening_node"
(str "Last block to end has name " ++ pr_id id' ++ str ".");
entry
- with Not_found -> error "There is nothing to end."
+ with Not_found -> user_err Pp.(str "There is nothing to end.")
(* Discharge tables *)
@@ -428,7 +428,7 @@ let add_section () =
let check_same_poly p vars =
let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
if List.exists pred vars then
- error "Cannot mix universe polymorphic and monomorphic declarations in sections."
+ user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.")
let add_section_variable id impl poly ctx =
match !sectab with
@@ -547,7 +547,7 @@ let discharge_item ((sp,_ as oname),e) =
| FrozenState _ -> None
| ClosedSection _ | ClosedModule _ -> None
| OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
- anomaly (Pp.str "discharge_item")
+ anomaly (Pp.str "discharge_item.")
let close_section () =
let oname,fs =
@@ -555,7 +555,7 @@ let close_section () =
| oname,OpenedSection (_,fs) -> oname,fs
| _ -> assert false
with Not_found ->
- error "No opened section."
+ user_err Pp.(str "No opened section.")
in
let (secdecls,mark,before) = split_lib_at_opening oname in
lib_state := { !lib_state with lib_stk = before };
diff --git a/library/libnames.ml b/library/libnames.ml
index dd74e192ff..50f28b0205 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -58,14 +58,14 @@ let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p)
let parse_dir s =
let len = String.length s in
let rec decoupe_dirs dirs n =
- if Int.equal n len && n > 0 then error (s ^ " is an invalid path.");
+ if Int.equal n len && n > 0 then user_err Pp.(str @@ s ^ " is an invalid path.");
if n >= len then dirs else
let pos =
try
String.index_from s n '.'
with Not_found -> len
in
- if Int.equal pos n then error (s ^ " is an invalid path.");
+ if Int.equal pos n then user_err Pp.(str @@ s ^ " is an invalid path.");
let dir = String.sub s n (pos-n) in
decoupe_dirs ((Id.of_string dir)::dirs) (pos+1)
in
diff --git a/library/library.ml b/library/library.ml
index 2b3381fa7c..5a5f99cc51 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -764,7 +764,7 @@ let save_library_to ?todo dir f otab =
if !Flags.native_compiler then
let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
if not (Nativelib.compile_library dir ast fn) then
- error "Could not compile the library to native code."
+ user_err Pp.(str "Could not compile the library to native code.")
with reraise ->
let reraise = CErrors.push reraise in
let () = Feedback.msg_warning (str "Removed file " ++ str f') in
diff --git a/library/library.mllib b/library/library.mllib
index df4f735034..6f433b77d1 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -16,3 +16,4 @@ Goptions
Decls
Heads
Keys
+Coqlib
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/nameops.ml b/library/nameops.ml
index 098f5112fd..0b5dfd8d0e 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Util
open Names
@@ -14,10 +13,6 @@ open Names
let pr_id id = Id.print id
-let pr_name = function
- | Anonymous -> str "_"
- | Name id -> pr_id id
-
(* Utilities *)
let code_of_0 = Char.code '0'
@@ -124,34 +119,82 @@ let atompart_of_id id = fst (repr_ident id)
(* Names *)
-let out_name = function
- | Name id -> id
- | Anonymous -> failwith "Nameops.out_name"
+module type ExtName =
+sig
+
+ include module type of struct include Names.Name end
+
+ exception IsAnonymous
+
+ val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a
+ val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a
+ val iter : (Id.t -> unit) -> t -> unit
+ val map : (Id.t -> Id.t) -> t -> t
+ val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t
+ val get_id : t -> Id.t
+ val pick : t -> t -> t
+ val cons : t -> Id.t list -> Id.t list
+ val to_option : Name.t -> Id.t option
+
+end
+
+module Name : ExtName =
+struct
+
+ include Names.Name
+
+ exception IsAnonymous
+
+ let fold_left f a = function
+ | Name id -> f a id
+ | Anonymous -> a
+
+ let fold_right f na a =
+ match na with
+ | Name id -> f id a
+ | Anonymous -> a
+
+ let iter f na = fold_right (fun x () -> f x) na ()
+
+ let map f = function
+ | Name id -> Name (f id)
+ | Anonymous -> Anonymous
+
+ let fold_map f a = function
+ | Name id -> let (a, id) = f a id in (a, Name id)
+ | Anonymous -> a, Anonymous
+
+ let get_id = function
+ | Name id -> id
+ | Anonymous -> raise IsAnonymous
-let name_fold f na a =
- match na with
- | Name id -> f id a
- | Anonymous -> a
+ let pick na1 na2 =
+ match na1 with
+ | Name _ -> na1
+ | Anonymous -> na2
-let name_iter f na = name_fold (fun x () -> f x) na ()
+ let cons na l =
+ match na with
+ | Anonymous -> l
+ | Name id -> id::l
-let name_cons na l =
- match na with
- | Anonymous -> l
- | Name id -> id::l
+ let to_option = function
+ | Anonymous -> None
+ | Name id -> Some id
-let name_app f = function
- | Name id -> Name (f id)
- | Anonymous -> Anonymous
+end
-let name_fold_map f e = function
- | Name id -> let (e,id) = f e id in (e,Name id)
- | Anonymous -> e,Anonymous
+open Name
-let name_max na1 na2 =
- match na1 with
- | Name _ -> na1
- | Anonymous -> na2
+(* Compatibility *)
+let out_name = get_id
+let name_fold = fold_right
+let name_iter = iter
+let name_app = map
+let name_fold_map = fold_map
+let name_cons = cons
+let name_max = pick
+let pr_name = print
let pr_lab l = Label.print l
diff --git a/library/nameops.mli b/library/nameops.mli
index 3a67b61a13..abfc09db8d 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -9,8 +9,6 @@
open Names
(** Identifiers and names *)
-val pr_id : Id.t -> Pp.std_ppcmds
-val pr_name : Name.t -> Pp.std_ppcmds
val make_ident : string -> int option -> Id.t
val repr_ident : Id.t -> string * int option
@@ -50,16 +48,69 @@ val increment_subscript : Id.t -> Id.t
val forget_subscript : Id.t -> Id.t
+module Name : sig
+
+ include module type of struct include Names.Name end
+
+ exception IsAnonymous
+
+ val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a
+ (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *)
+
+ val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
+ (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *)
+
+ val iter : (Id.t -> unit) -> Name.t -> unit
+ (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *)
+
+ val map : (Id.t -> Id.t) -> Name.t -> t
+ (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *)
+
+ val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
+ (** [fold_map f na a] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')].
+ It is [a,Anonymous] otherwise. *)
+
+ val get_id : Name.t -> Id.t
+ (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *)
+
+ val pick : Name.t -> Name.t -> Name.t
+ (** [pick na na'] returns [Anonymous] if both names are [Anonymous].
+ Pick one of [na] or [na'] otherwise. *)
+
+ val cons : Name.t -> Id.t list -> Id.t list
+ (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *)
+
+ val to_option : Name.t -> Id.t option
+ (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *)
+
+end
+
val out_name : Name.t -> Id.t
-(** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"]
- otherwise. *)
+(** @deprecated Same as [Name.get_id] *)
val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
+(** @deprecated Same as [Name.fold_right] *)
+
val name_iter : (Id.t -> unit) -> Name.t -> unit
-val name_cons : Name.t -> Id.t list -> Id.t list
+(** @deprecated Same as [Name.iter] *)
+
val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
+(** @deprecated Same as [Name.map] *)
+
val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
+(** @deprecated Same as [Name.fold_map] *)
+
val name_max : Name.t -> Name.t -> Name.t
+(** @deprecated Same as [Name.pick] *)
+
+val name_cons : Name.t -> Id.t list -> Id.t list
+(** @deprecated Same as [Name.cons] *)
+
+val pr_name : Name.t -> Pp.std_ppcmds
+(** @deprecated Same as [Name.print] *)
+
+val pr_id : Id.t -> Pp.std_ppcmds
+(** @deprecated Same as [Names.Id.print] *)
val pr_lab : Label.t -> Pp.std_ppcmds
diff --git a/library/nametab.ml b/library/nametab.ml
index 1027e291ce..93e9c03cee 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -143,8 +143,8 @@ struct
(* This is an absolute name, we must keep it otherwise it may
become unaccessible forever *)
(* But ours is also absolute! This is an error! *)
- error ("Cannot mask the absolute name \""
- ^ U.to_string uname' ^ "\"!")
+ user_err Pp.(str @@ "Cannot mask the absolute name \""
+ ^ U.to_string uname' ^ "\"!")
| Nothing
| Relative _ -> mktree (Absolute (uname,o)) tree.map
@@ -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-05-02 07:45:07 +0000