diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/dischargedhypsmap.ml | 21 | ||||
| -rw-r--r-- | library/dischargedhypsmap.mli | 19 | ||||
| -rw-r--r-- | library/global.ml | 4 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | library/goptions.ml | 2 | ||||
| -rw-r--r-- | library/library.mllib | 1 | ||||
| -rw-r--r-- | library/nametab.ml | 48 |
7 files changed, 12 insertions, 85 deletions
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/global.ml b/library/global.ml index e833f71142..5872126a12 100644 --- a/library/global.ml +++ b/library/global.ml @@ -271,8 +271,8 @@ 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) diff --git a/library/global.mli b/library/global.mli index 2819c187ed..6aeae9fd02 100644 --- a/library/global.mli +++ b/library/global.mli @@ -148,7 +148,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 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/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 |