diff options
Diffstat (limited to 'library/decl_kinds.ml')
| -rw-r--r-- | library/decl_kinds.ml | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 8ea183509..20808f1e6 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -9,10 +9,11 @@ (* $Id$ *) open Util +open Libnames (* Informal mathematical status of declarations *) -type locality_flag = (*bool (* local = true; global = false *)*) +type locality = | Local | Global @@ -40,8 +41,6 @@ type definition_object_kind = | IdentityCoercion | Instance -type strength = locality_flag (* For compatibility *) - type assumption_object_kind = Definitional | Logical | Conjectural (* [assumption_kind] @@ -52,9 +51,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality_flag * assumption_object_kind +type assumption_kind = locality * assumption_object_kind -type definition_kind = locality_flag * boxed_flag * definition_object_kind +type definition_kind = locality * boxed_flag * definition_object_kind (* Kinds used in proofs *) @@ -62,7 +61,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality_flag * goal_object_kind +type goal_kind = locality * goal_object_kind (* Kinds used in library *) @@ -100,3 +99,13 @@ let string_of_definition_kind (l,boxed,d) = anomaly "Unsupported local definition kind" | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Instance) -> 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" |