aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/decl_kinds.ml11
-rw-r--r--library/declaremods.ml7
-rw-r--r--library/declaremods.mli10
-rw-r--r--library/global.ml3
-rw-r--r--library/global.mli2
-rw-r--r--library/globnames.ml2
-rw-r--r--library/globnames.mli4
-rw-r--r--library/goptions.ml4
-rw-r--r--library/goptions.mli8
-rw-r--r--library/heads.ml2
-rw-r--r--library/keys.ml4
-rw-r--r--library/libnames.ml87
-rw-r--r--library/libnames.mli44
-rw-r--r--library/library.ml14
-rw-r--r--library/library.mli2
-rw-r--r--library/library.mllib1
-rw-r--r--library/misctypes.ml130
-rw-r--r--library/nametab.ml49
-rw-r--r--library/nametab.mli18
-rw-r--r--library/summary.ml44
-rw-r--r--library/summary.mli20
21 files changed, 98 insertions, 368 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 0d32853116..c1a673edf0 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -74,14 +74,3 @@ type logical_kind =
| IsAssumption of assumption_object_kind
| IsDefinition of definition_object_kind
| IsProof of theorem_kind
-
-(** Recursive power of type declarations *)
-
-type recursivity_kind = Declarations.recursivity_kind =
- | Finite (** = inductive *)
- [@ocaml.deprecated "Please use [Declarations.Finite"]
- | CoFinite (** = coinductive *)
- [@ocaml.deprecated "Please use [Declarations.CoFinite"]
- | BiFinite (** = non-recursive, like in "Record" definitions *)
- [@ocaml.deprecated "Please use [Declarations.BiFinite"]
-[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"]
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 1d5df49cfd..0b3b461e6c 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -17,7 +17,6 @@ open Entries
open Libnames
open Libobject
open Mod_subst
-open Misctypes
(** {6 Inlining levels} *)
@@ -36,6 +35,8 @@ type inline =
| DefaultInline
| InlineAt of int
+type module_kind = Module | ModType | ModAny
+
let default_inline () = Some (Flags.get_inline_level ())
let inl2intopt = function
@@ -994,8 +995,8 @@ let iter_all_segments f =
(** {6 Some types used to shorten declaremods.mli} *)
type 'modast module_interpretor =
- Environ.env -> Misctypes.module_kind -> 'modast ->
- Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
+ Environ.env -> module_kind -> 'modast ->
+ Entries.module_struct_entry * module_kind * Univ.ContextSet.t
type 'modast module_params =
(lident list * ('modast * inline)) list
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 4aee7feae9..b42a59bfbd 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -27,12 +27,16 @@ type inline =
| DefaultInline
| InlineAt of int
+(** Kinds of modules *)
+
+type module_kind = Module | ModType | ModAny
+
type 'modast module_interpretor =
- Environ.env -> Misctypes.module_kind -> 'modast ->
- Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
+ Environ.env -> module_kind -> 'modast ->
+ Entries.module_struct_entry * module_kind * Univ.ContextSet.t
type 'modast module_params =
- (Misctypes.lident list * ('modast * inline)) list
+ (lident list * ('modast * inline)) list
(** [declare_module interp_modast id fargs typ exprs]
declares module [id], with structure constructed by [interp_modast]
diff --git a/library/global.ml b/library/global.ml
index 6083c40794..dcb20a280e 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -259,6 +259,9 @@ let is_type_in_type r =
| IndRef ind -> Environ.type_in_type_ind ind env
| ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env
+let current_modpath () =
+ Safe_typing.current_modpath (safe_env ())
+
let current_dirpath () =
Safe_typing.current_dirpath (safe_env ())
diff --git a/library/global.mli b/library/global.mli
index 906d246eef..57e173cb93 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -157,6 +157,8 @@ val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
(* Modifies the global state, registering new universes *)
+val current_modpath : unit -> ModPath.t
+
val current_dirpath : unit -> DirPath.t
val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a
diff --git a/library/globnames.ml b/library/globnames.ml
index 6b78d12baf..6383a1f8f6 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -87,8 +87,6 @@ let printable_constr_of_global = function
| ConstructRef sp -> mkConstruct sp
| IndRef sp -> mkInd sp
-let reference_of_constr = global_of_constr
-
let global_eq_gen eq_cst eq_ind eq_cons x y =
x == y ||
match x, y with
diff --git a/library/globnames.mli b/library/globnames.mli
index 2fe35ebccd..15fcd5bdd9 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -49,10 +49,6 @@ val printable_constr_of_global : GlobRef.t -> constr
raise [Not_found] if not a global reference *)
val global_of_constr : constr -> GlobRef.t
-(** Obsolete synonyms for constr_of_global and global_of_constr *)
-val reference_of_constr : constr -> GlobRef.t
-[@@ocaml.deprecated "Alias of Globnames.global_of_constr"]
-
module RefOrdered : sig
type t = GlobRef.t
val compare : t -> t -> int
diff --git a/library/goptions.ml b/library/goptions.ml
index 76071ebcc2..f14ad333e9 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -161,7 +161,7 @@ module type RefConvertArg =
sig
type t
val compare : t -> t -> int
- val encode : reference -> t
+ val encode : qualid -> t
val subst : substitution -> t -> t
val printer : t -> Pp.t
val key : option_name
@@ -172,7 +172,7 @@ end
module RefConvert = functor (A : RefConvertArg) ->
struct
type t = A.t
- type key = reference
+ type key = qualid
let compare = A.compare
let table = ref_table
let encode = A.encode
diff --git a/library/goptions.mli b/library/goptions.mli
index 6c14d19ee9..3d7df18fed 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -89,7 +89,7 @@ module MakeRefTable :
(A : sig
type t
val compare : t -> t -> int
- val encode : reference -> t
+ val encode : qualid -> t
val subst : substitution -> t -> t
val printer : t -> Pp.t
val key : option_name
@@ -147,9 +147,9 @@ val get_string_table :
val get_ref_table :
option_name ->
- < add : reference -> unit;
- remove : reference -> unit;
- mem : reference -> unit;
+ < add : qualid -> unit;
+ remove : qualid -> unit;
+ mem : qualid -> unit;
print : unit >
(** The first argument is a locality flag. *)
diff --git a/library/heads.ml b/library/heads.ml
index 198672a0a1..d9d650ac07 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -129,7 +129,7 @@ let compute_head = function
let cb = Environ.lookup_constant cst env in
let is_Def = function Declarations.Def _ -> true | _ -> false in
let body =
- if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body
+ if not (Environ.is_projection cst env) && is_Def cb.Declarations.const_body
then Global.body_of_constant cst else None
in
(match body with
diff --git a/library/keys.ml b/library/keys.ml
index 89363455d7..3cadcb6472 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -11,9 +11,9 @@
(** Keys for unification and indexing *)
open Names
-open Term
-open Globnames
+open Constr
open Libobject
+open Globnames
type key =
| KGlob of GlobRef.t
diff --git a/library/libnames.ml b/library/libnames.ml
index 4ceea480d2..23085048a1 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -15,8 +15,6 @@ open Names
(**********************************************)
-let pr_dirpath sl = DirPath.print sl
-
(*s Operations on dirpaths *)
let split_dirpath d = match DirPath.repr d with
@@ -80,8 +78,6 @@ let dirpath_of_string s =
in
DirPath.make path
-let string_of_dirpath = Names.DirPath.to_string
-
module Dirset = Set.Make(DirPath)
module Dirmap = Map.Make(DirPath)
@@ -138,23 +134,33 @@ let restrict_path n sp =
make_path (DirPath.make dir') s
(*s qualified names *)
-type qualid = full_path
+type qualid_r = full_path
+type qualid = qualid_r CAst.t
-let make_qualid = make_path
-let repr_qualid = repr_path
+let make_qualid ?loc pa id = CAst.make ?loc (make_path pa id)
+let repr_qualid {CAst.v=qid} = repr_path qid
-let qualid_eq = eq_full_path
+let qualid_eq qid1 qid2 = eq_full_path qid1.CAst.v qid2.CAst.v
-let string_of_qualid = string_of_path
-let pr_qualid = pr_path
+let string_of_qualid qid = string_of_path qid.CAst.v
+let pr_qualid qid = pr_path qid.CAst.v
-let qualid_of_string = path_of_string
+let qualid_of_string ?loc s = CAst.make ?loc @@ path_of_string s
-let qualid_of_path sp = sp
-let qualid_of_ident id = make_qualid DirPath.empty id
-let qualid_of_dirpath dir =
+let qualid_of_path ?loc sp = CAst.make ?loc sp
+let qualid_of_ident ?loc id = make_qualid ?loc DirPath.empty id
+let qualid_of_dirpath ?loc dir =
let (l,a) = split_dirpath dir in
- make_qualid l a
+ make_qualid ?loc l a
+
+let qualid_is_ident qid =
+ DirPath.is_empty qid.CAst.v.dirpath
+
+let qualid_basename qid =
+ qid.CAst.v.basename
+
+let qualid_path qid =
+ qid.CAst.v.dirpath
type object_name = full_path * KerName.t
@@ -187,52 +193,6 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with
| DirModule op1, DirModule op2 -> eq_op op1 op2
| _ -> false
-type reference_r =
- | Qualid of qualid
- | Ident of Id.t
-type reference = reference_r CAst.t
-
-let qualid_of_reference = CAst.map (function
- | Qualid qid -> qid
- | Ident id -> qualid_of_ident id)
-
-let string_of_reference = CAst.with_val (function
- | Qualid qid -> string_of_qualid qid
- | Ident id -> Id.to_string id)
-
-let pr_reference = CAst.with_val (function
- | Qualid qid -> pr_qualid qid
- | Ident id -> Id.print id)
-
-let eq_reference {CAst.v=r1} {CAst.v=r2} = match r1, r2 with
-| Qualid q1, Qualid q2 -> qualid_eq q1 q2
-| Ident id1, Ident id2 -> Id.equal id1 id2
-| _ -> false
-
-let join_reference {CAst.loc=l1;v=ns} {CAst.loc=l2;v=r} =
- CAst.make ?loc:(Loc.merge_opt l1 l2) (
- match ns , r with
- Qualid q1, Qualid q2 ->
- let (dp1,id1) = repr_qualid q1 in
- let (dp2,id2) = repr_qualid q2 in
- Qualid (make_qualid
- (append_dirpath (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) dp2)
- id2)
- | Qualid q1, Ident id2 ->
- let (dp1,id1) = repr_qualid q1 in
- Qualid (make_qualid
- (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1)))
- id2)
- | Ident id1, Qualid q2 ->
- let (dp2,id2) = repr_qualid q2 in
- Qualid (make_qualid
- (append_dirpath (dirpath_of_string (Names.Id.to_string id1)) dp2)
- id2)
- | Ident id1, Ident id2 ->
- Qualid (make_qualid
- (dirpath_of_string (Names.Id.to_string id1)) id2)
- )
-
(* Default paths *)
let default_library = Names.DirPath.initial (* = ["Top"] *)
@@ -240,8 +200,3 @@ let default_library = Names.DirPath.initial (* = ["Top"] *)
let coq_string = "Coq"
let coq_root = Id.of_string coq_string
let default_root_prefix = DirPath.empty
-
-(* Deprecated synonyms *)
-
-let make_short_qualid = qualid_of_ident
-let qualid_of_sp = qualid_of_path
diff --git a/library/libnames.mli b/library/libnames.mli
index 81e5bc5b13..447eecbb5c 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -14,12 +14,6 @@ open Names
(** {6 Dirpaths } *)
val dirpath_of_string : string -> DirPath.t
-val pr_dirpath : DirPath.t -> Pp.t
-[@@ocaml.deprecated "Alias for DirPath.print"]
-
-val string_of_dirpath : DirPath.t -> string
-[@@ocaml.deprecated "Alias for DirPath.to_string"]
-
(** Pop the suffix of a [DirPath.t]. Raises a [Failure] for an empty path *)
val pop_dirpath : DirPath.t -> DirPath.t
@@ -71,23 +65,28 @@ val restrict_path : int -> full_path -> full_path
qualifications of absolute names, including single identifiers.
The [qualid] are used to access the name table. *)
-type qualid
+type qualid_r
+type qualid = qualid_r CAst.t
-val make_qualid : DirPath.t -> Id.t -> qualid
+val make_qualid : ?loc:Loc.t -> DirPath.t -> Id.t -> qualid
val repr_qualid : qualid -> DirPath.t * Id.t
val qualid_eq : qualid -> qualid -> bool
val pr_qualid : qualid -> Pp.t
val string_of_qualid : qualid -> string
-val qualid_of_string : string -> qualid
+val qualid_of_string : ?loc:Loc.t -> string -> qualid
(** Turns an absolute name, a dirpath, or an Id.t into a
qualified name denoting the same name *)
-val qualid_of_path : full_path -> qualid
-val qualid_of_dirpath : DirPath.t -> qualid
-val qualid_of_ident : Id.t -> qualid
+val qualid_of_path : ?loc:Loc.t -> full_path -> qualid
+val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid
+val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid
+
+val qualid_is_ident : qualid -> bool
+val qualid_path : qualid -> DirPath.t
+val qualid_basename : qualid -> Id.t
(** Both names are passed to objects: a "semantic" [kernel_name], which
can be substituted and a "syntactic" [full_path] which can be printed
@@ -130,20 +129,6 @@ val eq_global_dir_reference :
global_dir_reference -> global_dir_reference -> bool
(** {6 ... } *)
-(** A [reference] is the user-level notion of name. It denotes either a
- global name (referred either by a qualified name or by a single
- name) or a variable *)
-
-type reference_r =
- | Qualid of qualid
- | Ident of Id.t
-type reference = reference_r CAst.t
-
-val eq_reference : reference -> reference -> bool
-val qualid_of_reference : reference -> qualid CAst.t
-val string_of_reference : reference -> string
-val pr_reference : reference -> Pp.t
-val join_reference : reference -> reference -> reference
(** some preset paths *)
val default_library : DirPath.t
@@ -155,10 +140,3 @@ val coq_string : string (** "Coq" *)
(** This is the default root prefix for developments which doesn't
mention a root *)
val default_root_prefix : DirPath.t
-
-(** Deprecated synonyms *)
-val make_short_qualid : Id.t -> qualid (** = qualid_of_ident *)
-[@@ocaml.deprecated "Alias for qualid_of_ident"]
-
-val qualid_of_sp : full_path -> qualid (** = qualid_of_path *)
-[@@ocaml.deprecated "Alias for qualid_of_sp"]
diff --git a/library/library.ml b/library/library.ml
index 56d2709d5b..400f3dcf13 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -577,10 +577,10 @@ let require_library_from_dirpath modrefl export =
(* the function called by Vernacentries.vernac_import *)
-let safe_locate_module {CAst.loc;v=qid} =
+let safe_locate_module qid =
try Nametab.locate_module qid
with Not_found ->
- user_err ?loc ~hdr:"import_library"
+ user_err ?loc:qid.CAst.loc ~hdr:"import_library"
(pr_qualid qid ++ str " is not a module")
let import_module export modl =
@@ -595,18 +595,18 @@ let import_module export modl =
| [] -> ()
| modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
let rec aux acc = function
- | ({CAst.loc; v=dir} as m) :: l ->
+ | qid :: l ->
let m,acc =
- try Nametab.locate_module dir, acc
- with Not_found-> flush acc; safe_locate_module m, [] in
+ try Nametab.locate_module qid, acc
+ with Not_found-> flush acc; safe_locate_module qid, [] in
(match m with
| MPfile dir -> aux (dir::acc) l
| mp ->
flush acc;
try Declaremods.import_module export mp; aux [] l
with Not_found ->
- user_err ?loc ~hdr:"import_library"
- (pr_qualid dir ++ str " is not a module"))
+ user_err ?loc:qid.CAst.loc ~hdr:"import_library"
+ (pr_qualid qid ++ str " is not a module"))
| [] -> flush acc
in aux [] modl
diff --git a/library/library.mli b/library/library.mli
index 0877ebb5a9..d5815afc40 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -36,7 +36,7 @@ type seg_proofs = Constr.constr Future.computation array
(** Open a module (or a library); if the boolean is true then it's also
an export otherwise just a simple import *)
-val import_module : bool -> qualid CAst.t list -> unit
+val import_module : bool -> qualid list -> unit
(** Start the compilation of a file as a library. The first argument must be
output file, and the
diff --git a/library/library.mllib b/library/library.mllib
index 1c03688470..2ac4266fc0 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -6,7 +6,6 @@ Nametab
Global
Decl_kinds
Lib
-Misctypes
Declaremods
Loadpath
Library
diff --git a/library/misctypes.ml b/library/misctypes.ml
deleted file mode 100644
index b5d30559d8..0000000000
--- a/library/misctypes.ml
+++ /dev/null
@@ -1,130 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Names
-
-(** Basic types used both in [constr_expr], [glob_constr], and [vernacexpr] *)
-
-(** Located identifiers and objects with syntax. *)
-
-type lident = Id.t CAst.t
-type lname = Name.t CAst.t
-type lstring = string CAst.t
-
-(** Cases pattern variables *)
-
-type patvar = Id.t
-
-(** Introduction patterns *)
-
-type 'constr intro_pattern_expr =
- | IntroForthcoming of bool
- | IntroNaming of intro_pattern_naming_expr
- | IntroAction of 'constr intro_pattern_action_expr
-and intro_pattern_naming_expr =
- | IntroIdentifier of Id.t
- | IntroFresh of Id.t
- | IntroAnonymous
-and 'constr intro_pattern_action_expr =
- | IntroWildcard
- | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
- | IntroInjection of ('constr intro_pattern_expr) CAst.t list
- | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t
- | IntroRewrite of bool
-and 'constr or_and_intro_pattern_expr =
- | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list
- | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list
-
-(** Move destination for hypothesis *)
-
-type 'id move_location =
- | MoveAfter of 'id
- | MoveBefore of 'id
- | MoveFirst
- | MoveLast (** can be seen as "no move" when doing intro *)
-
-(** A synonym of [Evar.t], also defined in Term *)
-
-type existential_key = Evar.t
-
-(** Case style, shared with Term *)
-
-type case_style = Constr.case_style =
- | LetStyle
- | IfStyle
- | LetPatternStyle
- | MatchStyle
- | RegularStyle (** infer printing form from number of constructor *)
-[@@ocaml.deprecated "Alias for Constr.case_style"]
-
-(** Casts *)
-
-type 'a cast_type =
- | CastConv of 'a
- | CastVM of 'a
- | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
- | CastNative of 'a
-
-(** Bindings *)
-
-type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
-
-type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list
-
-type 'a bindings =
- | ImplicitBindings of 'a list
- | ExplicitBindings of 'a explicit_bindings
- | NoBindings
-
-type 'a with_bindings = 'a * 'a bindings
-
-
-(** Some utility types for parsing *)
-
-type 'a or_var =
- | ArgArg of 'a
- | ArgVar of lident
-
-type 'a and_short_name = 'a * lident option
-
-type 'a or_by_notation_r =
- | AN of 'a
- | ByNotation of (string * string option)
-
-type 'a or_by_notation = 'a or_by_notation_r CAst.t
-
-(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
- but this formulation avoids a useless dependency. *)
-
-
-(** Kinds of modules *)
-
-type module_kind = Module | ModType | ModAny
-
-(** Various flags *)
-
-type direction_flag = bool (* true = Left-to-right false = right-to-right *)
-type evars_flag = bool (* true = pose evars false = fail on evars *)
-type rec_flag = bool (* true = recursive false = not recursive *)
-type advanced_flag = bool (* true = advanced false = basic *)
-type letin_flag = bool (* true = use local def false = use Leibniz *)
-type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
-
-type multi =
- | Precisely of int
- | UpTo of int
- | RepeatStar
- | RepeatPlus
-
-type ('a, 'b) gen_universe_decl = {
- univdecl_instance : 'a; (* Declared universes *)
- univdecl_extensible_instance : bool; (* Can new universes be added *)
- univdecl_constraints : 'b; (* Declared constraints *)
- univdecl_extensible_constraints : bool (* Can new constraints be added *) }
diff --git a/library/nametab.ml b/library/nametab.ml
index 995f447061..a3b3ca6e74 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -18,8 +18,8 @@ open Globnames
exception GlobalizationError of qualid
-let error_global_not_found {CAst.loc;v} =
- Loc.raise ?loc (GlobalizationError v)
+let error_global_not_found qid =
+ Loc.raise ?loc:qid.CAst.loc (GlobalizationError qid)
(* The visibility can be registered either
- for all suffixes not shorter then a given int - when the object
@@ -69,7 +69,7 @@ module type NAMETREE = sig
val find : user_name -> t -> elt
val exists : user_name -> t -> bool
val user_name : qualid -> t -> user_name
- val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+ val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
val find_prefixes : qualid -> t -> elt list
end
@@ -220,7 +220,7 @@ let exists uname tab =
with
Not_found -> false
-let shortest_qualid ctx uname tab =
+let shortest_qualid ?loc ctx uname tab =
let id,dir = U.repr uname in
let hidden = Id.Set.mem id ctx in
let rec find_uname pos dir tree =
@@ -235,7 +235,7 @@ let shortest_qualid ctx uname tab =
in
let ptab = Id.Map.find id tab in
let found_dir = find_uname [] dir ptab in
- make_qualid (DirPath.make found_dir) id
+ make_qualid ?loc (DirPath.make found_dir) id
let push_node node l =
match node with
@@ -458,14 +458,13 @@ let global_of_path sp =
let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab
-let global ({CAst.loc;v=r} as lr)=
- let {CAst.loc; v} as qid = qualid_of_reference lr in
- try match locate_extended v with
+let global qid =
+ try match locate_extended qid with
| TrueGlobal ref -> ref
| SynDef _ ->
- user_err ?loc ~hdr:"global"
+ user_err ?loc:qid.CAst.loc ~hdr:"global"
(str "Unexpected reference to a notation: " ++
- pr_qualid v)
+ pr_qualid qid)
with Not_found ->
error_global_not_found qid
@@ -510,40 +509,40 @@ let path_of_universe mp =
(* Shortest qualid functions **********************************************)
-let shortest_qualid_of_global ctx ref =
+let shortest_qualid_of_global ?loc ctx ref =
match ref with
- | VarRef id -> make_qualid DirPath.empty id
+ | VarRef id -> make_qualid ?loc DirPath.empty id
| _ ->
let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
- ExtRefTab.shortest_qualid ctx sp !the_ccitab
+ ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
-let shortest_qualid_of_syndef ctx kn =
+let shortest_qualid_of_syndef ?loc ctx kn =
let sp = path_of_syndef kn in
- ExtRefTab.shortest_qualid ctx sp !the_ccitab
+ ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
-let shortest_qualid_of_module mp =
+let shortest_qualid_of_module ?loc mp =
let dir = MPmap.find mp !the_modrevtab in
- DirTab.shortest_qualid Id.Set.empty dir !the_dirtab
+ DirTab.shortest_qualid ?loc Id.Set.empty dir !the_dirtab
-let shortest_qualid_of_modtype kn =
+let shortest_qualid_of_modtype ?loc kn =
let sp = MPmap.find kn !the_modtyperevtab in
- MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab
+ MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab
-let shortest_qualid_of_universe kn =
+let shortest_qualid_of_universe ?loc kn =
let sp = UnivIdMap.find kn !the_univrevtab in
- UnivTab.shortest_qualid Id.Set.empty sp !the_univtab
+ UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab
let pr_global_env env ref =
try pr_qualid (shortest_qualid_of_global env ref)
with Not_found as e ->
if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
-let global_inductive ({CAst.loc; v=r} as lr) =
- match global lr with
+let global_inductive qid =
+ match global qid with
| IndRef ind -> ind
| ref ->
- user_err ?loc ~hdr:"global_inductive"
- (pr_reference lr ++ spc () ++ str "is not an inductive type")
+ user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+ (pr_qualid qid ++ spc () ++ str "is not an inductive type")
(********************************************************************)
diff --git a/library/nametab.mli b/library/nametab.mli
index 2ec73a9869..57e9141db9 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -61,7 +61,7 @@ open Globnames
exception GlobalizationError of qualid
(** Raises a globalization error *)
-val error_global_not_found : qualid CAst.t -> 'a
+val error_global_not_found : qualid -> 'a
(** {6 Register visibility of things } *)
@@ -105,8 +105,8 @@ val locate_universe : qualid -> universe_id
references, like [locate] and co, but raise a nice error message
in case of failure *)
-val global : reference -> GlobRef.t
-val global_inductive : reference -> inductive
+val global : qualid -> GlobRef.t
+val global_inductive : qualid -> inductive
(** These functions locate all global references with a given suffix;
if [qualid] is valid as such, it comes first in the list *)
@@ -168,11 +168,11 @@ val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t
Coq.A.B.x that denotes the same object.
@raise Not_found for unknown objects. *)
-val shortest_qualid_of_global : Id.Set.t -> GlobRef.t -> qualid
-val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid
-val shortest_qualid_of_modtype : ModPath.t -> qualid
-val shortest_qualid_of_module : ModPath.t -> qualid
-val shortest_qualid_of_universe : universe_id -> qualid
+val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
+val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
+val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
+val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid
(** Deprecated synonyms *)
@@ -207,7 +207,7 @@ module type NAMETREE = sig
val find : user_name -> t -> elt
val exists : user_name -> t -> bool
val user_name : qualid -> t -> user_name
- val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+ val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
val find_prefixes : qualid -> t -> elt list
end
diff --git a/library/summary.ml b/library/summary.ml
index 7ef19fbfb4..9b22945919 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -75,20 +75,6 @@ let freeze_summaries ~marshallable : frozen =
ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod;
}
-let unfreeze_single name state =
- let decl =
- try String.Map.find name !sum_map
- with
- | Not_found ->
- CErrors.anomaly Pp.(str "trying to unfreeze unregistered summary " ++ str name)
- in
- try decl.unfreeze_function state
- with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- Feedback.msg_warning
- Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]);
- iraise e
-
let warn_summary_out_of_scope =
let name = "summary-out-of-scope" in
let category = "dev" in
@@ -142,36 +128,6 @@ let remove_from_summary st tag =
let summaries = String.Map.remove id st.summaries in
{st with summaries}
-(** Selective freeze *)
-
-type frozen_bits = Dyn.t String.Map.t
-
-let freeze_summary ~marshallable ?(complement=false) ids =
- let sub_map = String.Map.filter (fun id _ -> complement <> List.(mem id ids)) !sum_map in
- String.Map.map (fun decl -> decl.freeze_function marshallable) sub_map
-
-let unfreeze_summary = String.Map.iter unfreeze_single
-
-let surgery_summary { summaries; ml_module } bits =
- let summaries =
- String.Map.fold (fun hash state sum -> String.Map.set hash state sum ) summaries bits in
- { summaries; ml_module }
-
-let project_summary { summaries; ml_module } ?(complement=false) ids =
- String.Map.filter (fun name _ -> complement <> List.(mem name ids)) summaries
-
-let pointer_equal l1 l2 =
- let ptr_equal d1 d2 =
- let Dyn.Dyn (t1, x1) = d1 in
- let Dyn.Dyn (t2, x2) = d2 in
- match Dyn.eq t1 t2 with
- | None -> false
- | Some Refl -> x1 == x2
- in
- let l1, l2 = String.Map.bindings l1, String.Map.bindings l2 in
- CList.for_all2eq
- (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2
-
(** All-in-one reference declaration + registration *)
let ref_tag ?(freeze=fun _ r -> r) ~name x =
diff --git a/library/summary.mli b/library/summary.mli
index ed6c26b190..7d91a79188 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -91,25 +91,5 @@ val modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen
val project_from_summary : frozen -> 'a Dyn.tag -> 'a
val remove_from_summary : frozen -> 'a Dyn.tag -> frozen
-(** The type [frozen_bits] is a snapshot of some of the registered
- tables. It is DEPRECATED in favor of the typed projection
- version. *)
-
-type frozen_bits
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-
-[@@@ocaml.warning "-3"]
-val freeze_summary : marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val unfreeze_summary : frozen_bits -> unit
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val surgery_summary : frozen -> frozen_bits -> frozen
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val pointer_equal : frozen_bits -> frozen_bits -> bool
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-[@@@ocaml.warning "+3"]
-
(** {6 Debug} *)
val dump : unit -> (int * string) list
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 02:29:08 +0000