diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/decl_kinds.ml | 10 | ||||
| -rw-r--r-- | library/decl_kinds.mli | 6 | ||||
| -rw-r--r-- | library/declare.ml | 3 |
3 files changed, 7 insertions, 12 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 5ae048d65..ba40f98c0 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -15,8 +15,6 @@ type locality = | Local | Global -type boxed_flag = bool - type theorem_kind = | Theorem | Lemma @@ -52,7 +50,7 @@ type assumption_object_kind = Definitional | Logical | Conjectural *) type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * boxed_flag * definition_object_kind +type definition_kind = locality * definition_object_kind (* Kinds used in proofs *) @@ -84,12 +82,12 @@ let string_of_theorem_kind = function | Proposition -> "Proposition" | Corollary -> "Corollary" -let string_of_definition_kind (l,boxed,d) = - match (l,d) with +let string_of_definition_kind def = + match def with | Local, Coercion -> "Coercion Local" | Global, Coercion -> "Coercion" | Local, Definition -> "Let" - | Global, Definition -> if boxed then "Boxed Definition" else "Definition" + | Global, Definition -> "Definition" | Local, SubClass -> "Local SubClass" | Global, SubClass -> "SubClass" | Global, CanonicalStructure -> "Canonical Structure" diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 6b03442f5..88ef763c9 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -15,8 +15,6 @@ type locality = | Local | Global -type boxed_flag = bool - type theorem_kind = | Theorem | Lemma @@ -52,7 +50,7 @@ type assumption_object_kind = Definitional | Logical | Conjectural *) type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * boxed_flag * definition_object_kind +type definition_kind = locality * definition_object_kind (** Kinds used in proofs *) @@ -74,7 +72,7 @@ type logical_kind = val logical_kind_of_goal_kind : goal_object_kind -> logical_kind val string_of_theorem_kind : theorem_kind -> string val string_of_definition_kind : - locality * boxed_flag * definition_object_kind -> string + locality * definition_object_kind -> string (** About locality *) diff --git a/library/declare.ml b/library/declare.ml index a9c463020..fa95fe313 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -160,8 +160,7 @@ let hcons_constant_declaration = function DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; const_entry_type = Option.map hcons1_constr ce.const_entry_type; - const_entry_opaque = ce.const_entry_opaque; - const_entry_boxed = ce.const_entry_boxed } + const_entry_opaque = ce.const_entry_opaque } | cd -> cd let declare_constant_common id dhyps (cd,kind) = |