diff options
Diffstat (limited to 'intf/decl_kinds.mli')
| -rw-r--r-- | intf/decl_kinds.mli | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli index 6a4e18833..c117baf3f 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.mli @@ -10,7 +10,10 @@ type locality = Discharge | Local | Global -type binding_kind = Explicit | Implicit +type implicit_status = Explicit | Implicit + +type binding_kind = implicit_status +(** @deprecated Alias type *) type polymorphic = bool @@ -49,9 +52,13 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality * polymorphic * assumption_object_kind +type 'a declaration_kind = { locality : locality; + polymorphic : bool; + object_kind : 'a } + +type assumption_kind = assumption_object_kind declaration_kind -type definition_kind = locality * polymorphic * definition_object_kind +type definition_kind = definition_object_kind declaration_kind (** Kinds used in proofs *) @@ -59,7 +66,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * polymorphic * goal_object_kind +type goal_kind = goal_object_kind declaration_kind (** Kinds used in library *) |