aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/decl_kinds.ml11
-rw-r--r--library/global.ml3
-rw-r--r--library/global.mli3
-rw-r--r--library/keys.ml162
-rw-r--r--library/keys.mli23
-rw-r--r--library/lib.ml10
-rw-r--r--library/lib.mli3
-rw-r--r--library/library.mllib2
8 files changed, 9 insertions, 208 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
deleted file mode 100644
index 17746645ee..0000000000
--- a/library/decl_kinds.ml
+++ /dev/null
@@ -1,11 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <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) *)
-(************************************************************************)
-
-type binding_kind = Explicit | Implicit
diff --git a/library/global.ml b/library/global.ml
index ca774dbd74..0fc9e11364 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -89,6 +89,9 @@ let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
let set_engagement c = globalize0 (Safe_typing.set_engagement c)
let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b)
let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
+let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c)
+let set_check_positive c = globalize0 (Safe_typing.set_check_positive c)
+let set_check_universes c = globalize0 (Safe_typing.set_check_universes c)
let typing_flags () = Environ.typing_flags (env ())
let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
diff --git a/library/global.mli b/library/global.mli
index d034bc4208..b089b7dd80 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -31,6 +31,9 @@ val named_context : unit -> Constr.named_context
val set_engagement : Declarations.engagement -> unit
val set_indices_matter : bool -> unit
val set_typing_flags : Declarations.typing_flags -> unit
+val set_check_guarded : bool -> unit
+val set_check_positive : bool -> unit
+val set_check_universes : bool -> unit
val typing_flags : unit -> Declarations.typing_flags
val make_sprop_cumulative : unit -> unit
val set_allow_sprop : bool -> unit
diff --git a/library/keys.ml b/library/keys.ml
deleted file mode 100644
index 9964992433..0000000000
--- a/library/keys.ml
+++ /dev/null
@@ -1,162 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <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) *)
-(************************************************************************)
-
-(** Keys for unification and indexing *)
-
-open Names
-open Constr
-open Libobject
-open Globnames
-
-type key =
- | KGlob of GlobRef.t
- | KLam
- | KLet
- | KProd
- | KSort
- | KCase
- | KFix
- | KCoFix
- | KRel
- | KInt
-
-module KeyOrdered = struct
- type t = key
-
- let hash gr =
- match gr with
- | KGlob gr -> 9 + GlobRef.Ordered.hash gr
- | KLam -> 0
- | KLet -> 1
- | KProd -> 2
- | KSort -> 3
- | KCase -> 4
- | KFix -> 5
- | KCoFix -> 6
- | KRel -> 7
- | KInt -> 8
-
- let compare gr1 gr2 =
- match gr1, gr2 with
- | 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 -> GlobRef.Ordered.equal gr1 gr2
- | _, KGlob _ -> false
- | KGlob _, _ -> false
- | k, k' -> k == k'
-end
-
-module Keymap = HMap.Make(KeyOrdered)
-module Keyset = Keymap.Set
-
-(* Mapping structure for references to be considered equivalent *)
-
-let keys = Summary.ref Keymap.empty ~name:"Keys_decl"
-
-let add_kv k v m =
- try Keymap.modify k (fun k' vs -> Keyset.add v vs) m
- with Not_found -> Keymap.add k (Keyset.singleton v) m
-
-let add_keys k v =
- keys := add_kv k v (add_kv v k !keys)
-
-let equiv_keys k k' =
- k == k' || KeyOrdered.equal k k' ||
- try Keyset.mem k' (Keymap.find k !keys)
- with Not_found -> false
-
-(** Registration of keys as an object *)
-
-let load_keys _ (_,(ref,ref')) =
- add_keys ref ref'
-
-let cache_keys o =
- load_keys 1 o
-
-let subst_key subst k =
- match k with
- | KGlob gr -> KGlob (subst_global_reference subst gr)
- | _ -> k
-
-let subst_keys (subst,(k,k')) =
- (subst_key subst k, subst_key subst k')
-
-let discharge_key = function
- | KGlob (GlobRef.VarRef _ as g) when Lib.is_in_section g -> None
- | x -> Some x
-
-let discharge_keys (_,(k,k')) =
- match discharge_key k, discharge_key k' with
- | Some x, Some y -> Some (x, y)
- | _ -> None
-
-type key_obj = key * key
-
-let inKeys : key_obj -> obj =
- declare_object @@ superglobal_object "KEYS"
- ~cache:cache_keys
- ~subst:(Some subst_keys)
- ~discharge:discharge_keys
-
-let declare_equiv_keys ref ref' =
- Lib.add_anonymous_leaf (inKeys (ref,ref'))
-
-let constr_key kind c =
- try
- let rec aux k =
- match kind k with
- | Const (c, _) -> KGlob (GlobRef.ConstRef c)
- | Ind (i, u) -> KGlob (GlobRef.IndRef i)
- | Construct (c,u) -> KGlob (GlobRef.ConstructRef c)
- | Var id -> KGlob (GlobRef.VarRef id)
- | App (f, _) -> aux f
- | Proj (p, _) -> KGlob (GlobRef.ConstRef (Projection.constant p))
- | Cast (p, _, _) -> aux p
- | Lambda _ -> KLam
- | Prod _ -> KProd
- | Case _ -> KCase
- | Fix _ -> KFix
- | CoFix _ -> KCoFix
- | Rel _ -> KRel
- | Meta _ -> raise Not_found
- | Evar _ -> raise Not_found
- | Sort _ -> KSort
- | LetIn _ -> KLet
- | Int _ -> KInt
- in Some (aux c)
- with Not_found -> None
-
-open Pp
-
-let pr_key pr_global = function
- | KGlob gr -> pr_global gr
- | KLam -> str"Lambda"
- | KLet -> str"Let"
- | KProd -> str"Product"
- | KSort -> str"Sort"
- | KCase -> str"Case"
- | KFix -> str"Fix"
- | KCoFix -> str"CoFix"
- | KRel -> str"Rel"
- | KInt -> str"Int"
-
-let pr_keyset pr_global v =
- prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)
-
-let pr_mapping pr_global k v =
- pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v
-
-let pr_keys pr_global =
- Keymap.fold (fun k v acc -> pr_mapping pr_global k v ++ fnl () ++ acc) !keys (mt())
diff --git a/library/keys.mli b/library/keys.mli
deleted file mode 100644
index a7adf7791b..0000000000
--- a/library/keys.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <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) *)
-(************************************************************************)
-
-type key
-
-val declare_equiv_keys : key -> key -> unit
-(** Declare two keys as being equivalent. *)
-
-val equiv_keys : key -> key -> bool
-(** Check equivalence of keys. *)
-
-val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
-(** Compute the head key of a term. *)
-
-val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t
-(** Pretty-print the mapping *)
diff --git a/library/lib.ml b/library/lib.ml
index 6b01eb07e9..3f51826315 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -441,9 +441,6 @@ let empty_section_data ~poly = {
let sectab =
Summary.ref ([] : section_data list) ~name:"section-context"
-let sec_implicits =
- Summary.ref Id.Map.empty ~name:"section-implicits"
-
let check_same_poly p sec =
if p != sec.sec_poly then
user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.")
@@ -452,14 +449,13 @@ let add_section ~poly () =
List.iter (fun tab -> check_same_poly poly tab) !sectab;
sectab := empty_section_data ~poly :: !sectab
-let add_section_variable ~name ~kind ~poly =
+let add_section_variable ~name ~poly =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
| s :: sl ->
List.iter (fun tab -> check_same_poly poly tab) !sectab;
let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in
- sectab := s :: sl;
- sec_implicits := Id.Map.add name kind !sec_implicits
+ sectab := s :: sl
let add_section_context ctx =
match !sectab with
@@ -576,8 +572,6 @@ let section_segment_of_reference = let open GlobRef in function
let variable_section_segment_of_reference gr =
(section_segment_of_reference gr).abstr_ctx
-let variable_section_kind id = Id.Map.get id !sec_implicits
-
let section_instance = let open GlobRef in function
| VarRef id ->
let eq = function
diff --git a/library/lib.mli b/library/lib.mli
index 7dc8b52282..9ffa69ef93 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -177,12 +177,11 @@ val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
val section_segment_of_reference : GlobRef.t -> abstr_info
val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context
-val variable_section_kind : Id.t -> Decl_kinds.binding_kind
val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
val is_in_section : GlobRef.t -> bool
-val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> unit
+val add_section_variable : name:Id.t -> poly:bool -> unit
val add_section_context : Univ.ContextSet.t -> unit
val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
diff --git a/library/library.mllib b/library/library.mllib
index 35af5fa43b..3b75438ccd 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -1,4 +1,3 @@
-Decl_kinds
Libnames
Globnames
Libobject
@@ -11,5 +10,4 @@ Library
States
Kindops
Goptions
-Keys
Coqlib
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 07:40:44 +0000