diff options
| author | Pierre-Marie Pédrot | 2019-06-09 14:20:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-09 14:20:17 +0200 |
| commit | 1f81679d117446d32fcad8012e5613cb2377b359 (patch) | |
| tree | 216bcc16b1cfce4d2a6ce1ce4356f3a5a7fffd0d /library/decl_kinds.ml | |
| parent | 73c2dc60ccd4d64506250a9c7476740e97ab022c (diff) | |
| parent | 1c52097ecfccd22b7515f0e197b747107874b372 (diff) | |
Merge PR #8726: More robust treatment of the Discharge status
Reviewed-by: aspiwack
Ack-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'library/decl_kinds.ml')
| -rw-r--r-- | library/decl_kinds.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 8d5c2fb687..39042e1ab7 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -12,7 +12,9 @@ type discharge = DoDischarge | NoDischarge -type locality = Discharge | Local | Global +type import_status = ImportDefaultBehavior | ImportNeedQualified + +type locality = Discharge | Global of import_status type binding_kind = Explicit | Implicit @@ -46,7 +48,7 @@ type definition_object_kind = | Method | Let -type assumption_object_kind = Definitional | Logical | Conjectural +type assumption_object_kind = Definitional | Logical | Conjectural | Context (* [assumption_kind] |