diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/decl_kinds.ml | 48 | ||||
| -rw-r--r-- | library/decls.ml | 51 | ||||
| -rw-r--r-- | library/decls.mli | 41 | ||||
| -rw-r--r-- | library/kindops.ml | 37 | ||||
| -rw-r--r-- | library/kindops.mli | 17 | ||||
| -rw-r--r-- | library/library.mllib | 3 |
6 files changed, 1 insertions, 196 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 6eb582baef..5c479255df 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -15,51 +15,3 @@ type binding_kind = Explicit | Implicit type private_flag = bool type cumulative_inductive_flag = bool - -type theorem_kind = - | Theorem - | Lemma - | Fact - | Remark - | Property - | Proposition - | Corollary - -type definition_object_kind = - | Definition - | Coercion - | SubClass - | CanonicalStructure - | Example - | Fixpoint - | CoFixpoint - | Scheme - | StructureComponent - | IdentityCoercion - | Instance - | Method - | Let - -type assumption_object_kind = Definitional | Logical | Conjectural | Context - -(* [assumption_kind] - - | Local | Global - ------------------------------------ - Definitional | Variable | Parameter - Logical | Hypothesis | Axiom - -*) -(** Kinds used in proofs *) - -type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind - -(** Kinds used in library *) - -type logical_kind = - | IsPrimitive - | IsAssumption of assumption_object_kind - | IsDefinition of definition_object_kind - | IsProof of theorem_kind diff --git a/library/decls.ml b/library/decls.ml deleted file mode 100644 index 5cb35323dd..0000000000 --- a/library/decls.ml +++ /dev/null @@ -1,51 +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) *) -(************************************************************************) - -(** This module registers tables for some non-logical informations - associated declarations *) - -open Names -open Decl_kinds -open Libnames - -(** Datas associated to section variables and local definitions *) - -type variable_data = { - path:DirPath.t; - opaque:bool; - univs:Univ.ContextSet.t; - poly:bool; - kind:logical_kind; -} - -let vartab = - Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" - -let add_variable_data id o = vartab := Id.Map.add id o !vartab - -let variable_path id = let {path} = Id.Map.find id !vartab in path -let variable_opacity id = let {opaque} = Id.Map.find id !vartab in opaque -let variable_kind id = let {kind} = Id.Map.find id !vartab in kind -let variable_context id = let {univs} = Id.Map.find id !vartab in univs -let variable_polymorphic id = let {poly} = Id.Map.find id !vartab in poly - -let variable_secpath id = - let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in - make_qualid dir id - -let variable_exists id = Id.Map.mem id !vartab - -(** Datas associated to global parameters and constants *) - -let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT" - -let add_constant_kind kn k = csttab := Cmap.add kn k !csttab - -let constant_kind kn = Cmap.find kn !csttab diff --git a/library/decls.mli b/library/decls.mli deleted file mode 100644 index f88958bb04..0000000000 --- a/library/decls.mli +++ /dev/null @@ -1,41 +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) *) -(************************************************************************) - -open Names -open Libnames -open Decl_kinds - -(** This module manages non-kernel informations about declarations. It - is either non-logical informations or logical informations that - have no place to be (yet) in the kernel *) - -(** Registration and access to the table of variable *) - -type variable_data = { - path:DirPath.t; - opaque:bool; - univs:Univ.ContextSet.t; - poly:bool; - kind:logical_kind; -} - -val add_variable_data : variable -> variable_data -> unit -val variable_path : variable -> DirPath.t -val variable_secpath : variable -> qualid -val variable_kind : variable -> logical_kind -val variable_opacity : variable -> bool -val variable_context : variable -> Univ.ContextSet.t -val variable_polymorphic : variable -> bool -val variable_exists : variable -> bool - -(** Registration and access to the table of constants *) - -val add_constant_kind : Constant.t -> logical_kind -> unit -val constant_kind : Constant.t -> logical_kind diff --git a/library/kindops.ml b/library/kindops.ml deleted file mode 100644 index 0bf55c62a9..0000000000 --- a/library/kindops.ml +++ /dev/null @@ -1,37 +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) *) -(************************************************************************) - -open Decl_kinds - -(** Operations about types defined in [Decl_kinds] *) - -let logical_kind_of_goal_kind = function - | DefinitionBody d -> IsDefinition d - | Proof s -> IsProof s - -let string_of_theorem_kind = function - | Theorem -> "Theorem" - | Lemma -> "Lemma" - | Fact -> "Fact" - | Remark -> "Remark" - | Property -> "Property" - | Proposition -> "Proposition" - | Corollary -> "Corollary" - -let string_of_definition_object_kind = function - | Definition -> "Definition" - | Example -> "Example" - | Coercion -> "Coercion" - | SubClass -> "SubClass" - | CanonicalStructure -> "Canonical Structure" - | Instance -> "Instance" - | Let -> "Let" - | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> - CErrors.anomaly (Pp.str "Internal definition kind.") diff --git a/library/kindops.mli b/library/kindops.mli deleted file mode 100644 index 3c9f2bb7c3..0000000000 --- a/library/kindops.mli +++ /dev/null @@ -1,17 +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) *) -(************************************************************************) - -open Decl_kinds - -(** Operations about types defined in [Decl_kinds] *) - -val logical_kind_of_goal_kind : goal_object_kind -> logical_kind -val string_of_theorem_kind : theorem_kind -> string -val string_of_definition_object_kind : definition_object_kind -> string diff --git a/library/library.mllib b/library/library.mllib index ef53471377..35af5fa43b 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,16 +1,15 @@ +Decl_kinds Libnames Globnames Libobject Summary Nametab Global -Decl_kinds Lib Declaremods Library States Kindops Goptions -Decls Keys Coqlib |