diff options
Diffstat (limited to 'intf/decl_kinds.ml')
| -rw-r--r-- | intf/decl_kinds.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml index a97758833..1dea6d9e9 100644 --- a/intf/decl_kinds.ml +++ b/intf/decl_kinds.ml @@ -8,6 +8,8 @@ (** Informal mathematical status of declarations *) +type discharge = DoDischarge | NoDischarge + type locality = Discharge | Local | Global type binding_kind = Explicit | Implicit @@ -40,6 +42,7 @@ type definition_object_kind = | IdentityCoercion | Instance | Method + | Let type assumption_object_kind = Definitional | Logical | Conjectural |