diff options
Diffstat (limited to 'library/kindops.ml')
-rw-r--r-- | library/kindops.ml | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/library/kindops.ml b/library/kindops.ml new file mode 100644 index 00000000..56048647 --- /dev/null +++ b/library/kindops.ml @@ -0,0 +1,67 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +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_kind def = + let (locality, poly, kind) = def in + let error () = Errors.anomaly (Pp.str "Internal definition kind") in + match kind with + | Definition -> + begin match locality with + | Discharge -> "Let" + | Local -> "Local Definition" + | Global -> "Definition" + end + | Example -> + begin match locality with + | Discharge -> error () + | Local -> "Local Example" + | Global -> "Example" + end + | Coercion -> + begin match locality with + | Discharge -> error () + | Local -> "Local Coercion" + | Global -> "Coercion" + end + | SubClass -> + begin match locality with + | Discharge -> error () + | Local -> "Local SubClass" + | Global -> "SubClass" + end + | CanonicalStructure -> + begin match locality with + | Discharge -> error () + | Local -> error () + | Global -> "Canonical Structure" + end + | Instance -> + begin match locality with + | Discharge -> error () + | Local -> "Instance" + | Global -> "Global Instance" + end + | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> + Errors.anomaly (Pp.str "Internal definition kind") |