From 69929de6eccf6d60886ea0795376e9288863fc1f Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:08:17 +0000 Subject: Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15368 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/decl_kinds.ml | 126 ------------------------------------------------- library/decl_kinds.mli | 91 ----------------------------------- library/kindops.ml | 41 ++++++++++++++++ library/kindops.mli | 16 +++++++ library/library.mllib | 2 +- 5 files changed, 58 insertions(+), 218 deletions(-) delete mode 100644 library/decl_kinds.ml delete mode 100644 library/decl_kinds.mli create mode 100644 library/kindops.ml create mode 100644 library/kindops.mli (limited to 'library') diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml deleted file mode 100644 index e8734cbaae..0000000000 --- a/library/decl_kinds.ml +++ /dev/null @@ -1,126 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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_kind def = - match def with - | Local, Coercion -> "Coercion Local" - | Global, Coercion -> "Coercion" - | Local, Definition -> "Let" - | Global, Definition -> "Definition" - | Local, SubClass -> "Local SubClass" - | Global, SubClass -> "SubClass" - | Global, CanonicalStructure -> "Canonical Structure" - | Global, Example -> "Example" - | Local, (CanonicalStructure|Example) -> - anomaly "Unsupported local definition kind" - | Local, Instance -> "Instance" - | Global, Instance -> "Global Instance" - | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) - -> anomaly "Internal definition kind" - -(* Strength *) - -let strength_of_global = function - | VarRef _ -> Local - | IndRef _ | ConstructRef _ | ConstRef _ -> Global - -let string_of_strength = function - | Local -> "Local" - | Global -> "Global" - - -(* Recursive power *) - -(* spiwack: this definition might be of use in the kernel, for now I do not - push them deeper than needed, though. *) -type recursivity_kind = - | Finite (* = inductive *) - | CoFinite (* = coinductive *) - | BiFinite (* = non-recursive, like in "Record" definitions *) - -(* helper, converts to "finiteness flag" booleans *) -let recursivity_flag_of_kind = function - | Finite | BiFinite -> true - | CoFinite -> false diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli deleted file mode 100644 index 5b81d54ee5..0000000000 --- a/library/decl_kinds.mli +++ /dev/null @@ -1,91 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* logical_kind -val string_of_theorem_kind : theorem_kind -> string -val string_of_definition_kind : - locality * definition_object_kind -> string - -(** About locality *) - -val strength_of_global : global_reference -> locality -val string_of_strength : locality -> string - -(** About recursive power of type declarations *) - -type recursivity_kind = - | Finite (** = inductive *) - | CoFinite (** = coinductive *) - | BiFinite (** = non-recursive, like in "Record" definitions *) - -(** helper, converts to "finiteness flag" booleans *) -val recursivity_flag_of_kind : recursivity_kind -> bool diff --git a/library/kindops.ml b/library/kindops.ml new file mode 100644 index 0000000000..012e599e21 --- /dev/null +++ b/library/kindops.ml @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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_kind def = + match def with + | Local, Coercion -> "Coercion Local" + | Global, Coercion -> "Coercion" + | Local, Definition -> "Let" + | Global, Definition -> "Definition" + | Local, SubClass -> "Local SubClass" + | Global, SubClass -> "SubClass" + | Global, CanonicalStructure -> "Canonical Structure" + | Global, Example -> "Example" + | Local, (CanonicalStructure|Example) -> + Errors.anomaly "Unsupported local definition kind" + | Local, Instance -> "Instance" + | Global, Instance -> "Global Instance" + | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) + -> Errors.anomaly "Internal definition kind" diff --git a/library/kindops.mli b/library/kindops.mli new file mode 100644 index 0000000000..c7f2a2e7f9 --- /dev/null +++ b/library/kindops.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* logical_kind +val string_of_theorem_kind : theorem_kind -> string +val string_of_definition_kind : + locality * definition_object_kind -> string diff --git a/library/library.mllib b/library/library.mllib index e8b5a7a4c2..edd5bfc071 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -8,7 +8,7 @@ Lib Declaremods Library States -Decl_kinds +Kindops Dischargedhypsmap Goptions Decls -- cgit v1.2.3