aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml8
-rw-r--r--library/coqlib.mli8
-rw-r--r--library/dischargedhypsmap.ml21
-rw-r--r--library/dischargedhypsmap.mli19
-rw-r--r--library/dune9
-rw-r--r--library/global.ml12
-rw-r--r--library/global.mli6
-rw-r--r--library/globnames.ml69
-rw-r--r--library/globnames.mli31
-rw-r--r--library/goptions.ml2
-rw-r--r--library/keys.ml6
-rw-r--r--library/lib.ml15
-rw-r--r--library/lib.mli2
-rw-r--r--library/library.mllib1
-rw-r--r--library/nametab.ml48
15 files changed, 85 insertions, 172 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 408e259196..026b7aa316 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -47,7 +47,7 @@ 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 all = List.sort_uniquize GlobRef.Ordered_env.compare all in
let these = List.filter (has_suffix_in_dirs dirs) all in
match these with
| [x] -> x
@@ -349,6 +349,9 @@ 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"
+let coq_prod = lazy_init_reference ["Datatypes"] "prod"
+let coq_pair = lazy_init_reference ["Datatypes"] "pair"
+
(* Runtime part *)
let build_coq_True () = Lazy.force coq_True
let build_coq_I () = Lazy.force coq_I
@@ -364,6 +367,9 @@ 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
+let build_coq_prod () = Lazy.force coq_prod
+let build_coq_pair () = Lazy.force coq_pair
+
(* The following is less readable but does not depend on parsing *)
let coq_eq_ref = lazy (init_reference ["Logic"] "eq")
diff --git a/library/coqlib.mli b/library/coqlib.mli
index b4bd1b0e06..8844684957 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -101,7 +101,7 @@ val glob_jmeq : GlobRef.t
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
+ forced with [delayed_force] to get the actual constr or pattern
at runtime. *)
type coq_bool_data = {
@@ -167,7 +167,7 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed
val build_coq_sumbool : GlobRef.t delayed
(** {6 ... } *)
-(** Connectives
+(** Connectives
The False proposition *)
val build_coq_False : GlobRef.t delayed
@@ -186,6 +186,10 @@ val build_coq_iff : GlobRef.t delayed
val build_coq_iff_left_proj : GlobRef.t delayed
val build_coq_iff_right_proj : GlobRef.t delayed
+(** Pairs *)
+val build_coq_prod : GlobRef.t delayed
+val build_coq_pair : GlobRef.t delayed
+
(** Disjunction *)
val build_coq_or : GlobRef.t delayed
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
deleted file mode 100644
index abcdb93a27..0000000000
--- a/library/dischargedhypsmap.ml
+++ /dev/null
@@ -1,21 +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 Libnames
-
-type discharged_hyps = full_path list
-
-let discharged_hyps_map = Summary.ref Spmap.empty ~name:"discharged_hypothesis"
-
-let set_discharged_hyps sp hyps =
- discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
-
-let get_discharged_hyps sp =
- try Spmap.find sp !discharged_hyps_map with Not_found -> []
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
deleted file mode 100644
index c70677225b..0000000000
--- a/library/dischargedhypsmap.mli
+++ /dev/null
@@ -1,19 +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 Libnames
-
-type discharged_hyps = full_path list
-
-(** Discharged hypothesis. Here we store the discharged hypothesis of each
- constant or inductive type declaration. *)
-
-val set_discharged_hyps : full_path -> discharged_hyps -> unit
-val get_discharged_hyps : full_path -> discharged_hyps
diff --git a/library/dune b/library/dune
new file mode 100644
index 0000000000..344fad5a75
--- /dev/null
+++ b/library/dune
@@ -0,0 +1,9 @@
+(library
+ (name library)
+ (synopsis "Coq's Loadable Libraries (vo) Support")
+ (public_name coq.library)
+ (wrapped false)
+ (libraries kernel))
+
+(documentation
+ (package coq))
diff --git a/library/global.ml b/library/global.ml
index dcb20a280e..e872d081d6 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -86,10 +86,10 @@ let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
let push_named_def d = globalize0 (Safe_typing.push_named_def d)
let add_constraints c = globalize0 (Safe_typing.add_constraints c)
let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
-let push_context b c = globalize0 (Safe_typing.push_context b c)
let set_engagement c = globalize0 (Safe_typing.set_engagement c)
let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
+let typing_flags () = Environ.typing_flags (env ())
let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
@@ -270,11 +270,17 @@ let with_global f =
push_context_set false ctx; a
(* spiwack: register/unregister functions for retroknowledge *)
-let register field value by_clause =
- globalize0 (Safe_typing.register field value by_clause)
+let register field value =
+ globalize0 (Safe_typing.register field value)
let register_inline c = globalize0 (Safe_typing.register_inline c)
let set_strategy k l =
GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l)
+let set_reduction_sharing b =
+ let env = safe_env () in
+ let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in
+ let flags = { flags with Declarations.share_reduction = b } in
+ let env = Safe_typing.set_typing_flags flags env in
+ GlobalSafeEnv.set_safe_env env
diff --git a/library/global.mli b/library/global.mli
index b2a191ceeb..5205968c7b 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -30,6 +30,7 @@ val named_context : unit -> Constr.named_context
(** Changing the (im)predicativity of the system *)
val set_engagement : Declarations.engagement -> unit
val set_typing_flags : Declarations.typing_flags -> unit
+val typing_flags : unit -> Declarations.typing_flags
(** Variables, Local definitions, constants, inductive types *)
@@ -48,7 +49,6 @@ val add_mind :
(** Extra universe constraints *)
val add_constraints : Univ.Constraint.t -> unit
-val push_context : bool -> Univ.UContext.t -> unit
val push_context_set : bool -> Univ.ContextSet.t -> unit
(** Non-interactive modules and module types *)
@@ -147,7 +147,7 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t
(** {6 Retroknowledge } *)
val register :
- Retroknowledge.field -> Constr.constr -> Constr.constr -> unit
+ Retroknowledge.field -> GlobRef.t -> unit
val register_inline : Constant.t -> unit
@@ -155,6 +155,8 @@ val register_inline : Constant.t -> unit
val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
+val set_reduction_sharing : bool -> unit
+
(* Modifies the global state, registering new universes *)
val current_modpath : unit -> ModPath.t
diff --git a/library/globnames.ml b/library/globnames.ml
index 6383a1f8f6..6bbdd36489 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -87,65 +87,14 @@ let printable_constr_of_global = function
| ConstructRef sp -> mkConstruct sp
| IndRef sp -> mkInd sp
-let global_eq_gen eq_cst eq_ind eq_cons x y =
- x == y ||
- match x, y with
- | ConstRef cx, ConstRef cy -> eq_cst cx cy
- | IndRef indx, IndRef indy -> eq_ind indx indy
- | ConstructRef consx, ConstructRef consy -> eq_cons consx consy
- | VarRef v1, VarRef v2 -> Id.equal v1 v2
- | (VarRef _ | ConstRef _ | IndRef _ | ConstructRef _), _ -> false
-
-let global_ord_gen ord_cst ord_ind ord_cons x y =
- if x == y then 0
- else match x, y with
- | VarRef v1, VarRef v2 -> Id.compare v1 v2
- | VarRef _, _ -> -1
- | _, VarRef _ -> 1
- | ConstRef cx, ConstRef cy -> ord_cst cx cy
- | ConstRef _, _ -> -1
- | _, ConstRef _ -> 1
- | IndRef indx, IndRef indy -> ord_ind indx indy
- | IndRef _, _ -> -1
- | _ , IndRef _ -> 1
- | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
-
-let global_hash_gen hash_cst hash_ind hash_cons gr =
- let open Hashset.Combine in
- match gr with
- | ConstRef c -> combinesmall 1 (hash_cst c)
- | IndRef i -> combinesmall 2 (hash_ind i)
- | ConstructRef c -> combinesmall 3 (hash_cons c)
- | VarRef id -> combinesmall 4 (Id.hash id)
-
-(* By default, [global_reference] are ordered on their canonical part *)
-
-module RefOrdered = struct
- open Constant.CanOrd
- type t = global_reference
- let compare gr1 gr2 =
- global_ord_gen compare ind_ord constructor_ord gr1 gr2
- let equal gr1 gr2 = global_eq_gen equal eq_ind eq_constructor gr1 gr2
- let hash gr = global_hash_gen hash ind_hash constructor_hash gr
-end
-
-module RefOrdered_env = struct
- open Constant.UserOrd
- type t = global_reference
- let compare gr1 gr2 =
- global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2
- let equal gr1 gr2 =
- global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2
- let hash gr = global_hash_gen hash ind_user_hash constructor_user_hash gr
-end
-
-module Refmap = HMap.Make(RefOrdered)
-module Refset = Refmap.Set
+module RefOrdered = Names.GlobRef.Ordered
+module RefOrdered_env = Names.GlobRef.Ordered_env
-(* Alternative sets and maps indexed by the user part of the kernel names *)
+module Refmap = Names.GlobRef.Map
+module Refset = Names.GlobRef.Set
-module Refmap_env = HMap.Make(RefOrdered_env)
-module Refset_env = Refmap_env.Set
+module Refmap_env = Names.GlobRef.Map_env
+module Refset_env = Names.GlobRef.Set_env
(* Extended global references *)
@@ -164,14 +113,14 @@ module ExtRefOrdered = struct
let equal x y =
x == y ||
match x, y with
- | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.equal rx ry
+ | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.equal rx ry
| SynDef knx, SynDef kny -> KerName.equal knx kny
| (TrueGlobal _ | SynDef _), _ -> false
let compare x y =
if x == y then 0
else match x, y with
- | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.compare rx ry
+ | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.compare rx ry
| SynDef knx, SynDef kny -> KerName.compare knx kny
| TrueGlobal _, SynDef _ -> -1
| SynDef _, TrueGlobal _ -> 1
@@ -179,7 +128,7 @@ module ExtRefOrdered = struct
open Hashset.Combine
let hash = function
- | TrueGlobal gr -> combinesmall 1 (RefOrdered_env.hash gr)
+ | TrueGlobal gr -> combinesmall 1 (GlobRef.Ordered_env.hash gr)
| SynDef kn -> combinesmall 2 (KerName.hash kn)
end
diff --git a/library/globnames.mli b/library/globnames.mli
index 15fcd5bdd9..45ee069b06 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Util
open Names
open Constr
open Mod_subst
@@ -49,27 +48,21 @@ val printable_constr_of_global : GlobRef.t -> constr
raise [Not_found] if not a global reference *)
val global_of_constr : constr -> GlobRef.t
-module RefOrdered : sig
- type t = GlobRef.t
- val compare : t -> t -> int
- val equal : t -> t -> bool
- val hash : t -> int
-end
+module RefOrdered = Names.GlobRef.Ordered
+[@@ocaml.deprecated "Use Names.GlobRef.Ordered"]
-module RefOrdered_env : sig
- type t = GlobRef.t
- val compare : t -> t -> int
- val equal : t -> t -> bool
- val hash : t -> int
-end
+module RefOrdered_env = Names.GlobRef.Ordered_env
+[@@ocaml.deprecated "Use Names.GlobRef.Ordered_env"]
-module Refset : CSig.SetS with type elt = GlobRef.t
-module Refmap : Map.ExtS
- with type key = GlobRef.t and module Set := Refset
+module Refset = Names.GlobRef.Set
+[@@ocaml.deprecated "Use Names.GlobRef.Set"]
+module Refmap = Names.GlobRef.Map
+[@@ocaml.deprecated "Use Names.GlobRef.Map"]
-module Refset_env : CSig.SetS with type elt = GlobRef.t
-module Refmap_env : Map.ExtS
- with type key = GlobRef.t and module Set := Refset_env
+module Refset_env = GlobRef.Set_env
+[@@ocaml.deprecated "Use Names.GlobRef.Set_env"]
+module Refmap_env = GlobRef.Map_env
+[@@ocaml.deprecated "Use Names.GlobRef.Map_env"]
(** {6 Extended global references } *)
diff --git a/library/goptions.ml b/library/goptions.ml
index eafcb8fea6..dcbc46ab72 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -412,7 +412,7 @@ let print_tables () =
if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
else msg ++ fnl ()
in
- str "Synchronous options:" ++ fnl () ++
+ str "Options:" ++ fnl () ++
OptionMap.fold
(fun key (name, depr, (read,_,_)) p ->
p ++ print_option key name (read ()) depr)
diff --git a/library/keys.ml b/library/keys.ml
index 3cadcb6472..a74d13c600 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -31,7 +31,7 @@ module KeyOrdered = struct
let hash gr =
match gr with
- | KGlob gr -> 8 + RefOrdered.hash gr
+ | KGlob gr -> 8 + GlobRef.Ordered.hash gr
| KLam -> 0
| KLet -> 1
| KProd -> 2
@@ -43,14 +43,14 @@ module KeyOrdered = struct
let compare gr1 gr2 =
match gr1, gr2 with
- | KGlob gr1, KGlob gr2 -> RefOrdered.compare gr1 gr2
+ | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2
| _, KGlob _ -> -1
| KGlob _, _ -> 1
| k, k' -> Int.compare (hash k) (hash k')
let equal k1 k2 =
match k1, k2 with
- | KGlob gr1, KGlob gr2 -> RefOrdered.equal gr1 gr2
+ | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2
| _, KGlob _ -> false
| KGlob _, _ -> false
| k, k' -> k == k'
diff --git a/library/lib.ml b/library/lib.ml
index 8ebe44890c..07026a9c2a 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -440,6 +440,21 @@ let add_section_context ctx =
check_same_poly true vars;
sectab := (Context ctx :: vars,repl,abs)::sl
+exception PolyFound of bool (* make this a let exception once possible *)
+let is_polymorphic_univ u =
+ try
+ let open Univ in
+ List.iter (fun (vars,_,_) ->
+ List.iter (function
+ | Variable (_,_,poly,(univs,_)) ->
+ if LSet.mem u univs then raise (PolyFound poly)
+ | Context (univs,_) ->
+ if LSet.mem u univs then raise (PolyFound true)
+ ) vars
+ ) !sectab;
+ false
+ with PolyFound b -> b
+
let extract_hyps (secs,ohyps) =
let rec aux = function
| (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
diff --git a/library/lib.mli b/library/lib.mli
index 9933b762ba..a7d21060e9 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -183,6 +183,8 @@ val add_section_kn : Decl_kinds.polymorphic ->
MutInd.t -> Constr.named_context -> unit
val replacement_context : unit -> Opaqueproof.work_list
+val is_polymorphic_univ : Univ.Level.t -> bool
+
(** {6 Discharge: decrease the section level if in the current section } *)
val discharge_kn : MutInd.t -> MutInd.t
diff --git a/library/library.mllib b/library/library.mllib
index 9cacaba4a7..8f694f4a31 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -11,7 +11,6 @@ Loadpath
Library
States
Kindops
-Dischargedhypsmap
Goptions
Decls
Keys
diff --git a/library/nametab.ml b/library/nametab.ml
index a3b3ca6e74..840cf8e380 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -279,10 +279,10 @@ module ExtRefTab = Make(FullPath)(ExtRefEqual)
module MPTab = Make(FullPath)(MPEqual)
type ccitab = ExtRefTab.t
-let the_ccitab = ref (ExtRefTab.empty : ccitab)
+let the_ccitab = Summary.ref ~name:"ccitab" (ExtRefTab.empty : ccitab)
type mptab = MPTab.t
-let the_modtypetab = ref (MPTab.empty : mptab)
+let the_modtypetab = Summary.ref ~name:"modtypetab" (MPTab.empty : mptab)
module DirPath' =
struct
@@ -303,7 +303,7 @@ module DirTab = Make(DirPath')(GlobDir)
(* If we have a (closed) module M having a submodule N, than N does not
have the entry in [the_dirtab]. *)
type dirtab = DirTab.t
-let the_dirtab = ref (DirTab.empty : dirtab)
+let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab)
type universe_id = DirPath.t * int
@@ -314,7 +314,7 @@ struct
end
module UnivTab = Make(FullPath)(UnivIdEqual)
type univtab = UnivTab.t
-let the_univtab = ref (UnivTab.empty : univtab)
+let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)
(* Reversed name tables ***************************************************)
@@ -322,14 +322,14 @@ let the_univtab = ref (UnivTab.empty : univtab)
module Globrevtab = HMap.Make(ExtRefOrdered)
type globrevtab = full_path Globrevtab.t
-let the_globrevtab = ref (Globrevtab.empty : globrevtab)
+let the_globrevtab = Summary.ref ~name:"globrevtab" (Globrevtab.empty : globrevtab)
type mprevtab = DirPath.t MPmap.t
-let the_modrevtab = ref (MPmap.empty : mprevtab)
+let the_modrevtab = Summary.ref ~name:"modrevtab" (MPmap.empty : mprevtab)
type mptrevtab = full_path MPmap.t
-let the_modtyperevtab = ref (MPmap.empty : mptrevtab)
+let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevtab)
module UnivIdOrdered =
struct
@@ -344,7 +344,7 @@ end
module UnivIdMap = HMap.Make(UnivIdOrdered)
type univrevtab = full_path UnivIdMap.t
-let the_univrevtab = ref (UnivIdMap.empty : univrevtab)
+let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevtab)
(* Push functions *********************************************************)
@@ -546,38 +546,6 @@ let global_inductive qid =
(********************************************************************)
-(********************************************************************)
-(* Registration of tables as a global table and rollback *)
-
-type frozen = ccitab * dirtab * mptab * univtab
- * globrevtab * mprevtab * mptrevtab * univrevtab
-
-let freeze _ : frozen =
- !the_ccitab,
- !the_dirtab,
- !the_modtypetab,
- !the_univtab,
- !the_globrevtab,
- !the_modrevtab,
- !the_modtyperevtab,
- !the_univrevtab
-
-let unfreeze (ccit,dirt,mtyt,univt,globr,modr,mtyr,univr) =
- the_ccitab := ccit;
- the_dirtab := dirt;
- the_modtypetab := mtyt;
- the_univtab := univt;
- the_globrevtab := globr;
- the_modrevtab := modr;
- the_modtyperevtab := mtyr;
- the_univrevtab := univr
-
-let _ =
- Summary.declare_summary "names"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = Summary.nop }
-
(* Deprecated synonyms *)
let extended_locate = locate_extended
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 19:19:24 +0000