diff options
| author | Emilio Jesus Gallego Arias | 2020-05-04 11:18:34 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-18 19:08:19 +0200 |
| commit | c8b54d74bc7cf29cc04d0a3cedbf4a106f6e744c (patch) | |
| tree | 18a0bf70119a51f0bf6ec6262ddfefd9790b8005 /vernac/locality.mli | |
| parent | 809291d5ef7371bfe8841b95126c0332da55578f (diff) | |
[declare] Merge `DeclareObl` into `Declare`
This is needed as a first step to refactor and unify the obligation
save path and state; in particular `Equations` is a heavy user of
Hooks to modify obligations state, thus in order to make the hook
aware of this we need to place the obligation state before the hook.
As a good side-effect, `inline_private_constants` and `Hook.call` are
not exported from `Declare` anymore.
Diffstat (limited to 'vernac/locality.mli')
| -rw-r--r-- | vernac/locality.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/vernac/locality.mli b/vernac/locality.mli index bf65579efd..81da895568 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -10,6 +10,9 @@ (** * Managing locality *) +type import_status = ImportDefaultBehavior | ImportNeedQualified +type locality = Discharge | Global of import_status + (** * Positioning locality for commands supporting discharging and export outside of modules *) @@ -20,7 +23,7 @@ val make_locality : bool option -> bool val make_non_locality : bool option -> bool -val enforce_locality_exp : bool option -> Vernacexpr.discharge -> Declare.locality +val enforce_locality_exp : bool option -> Vernacexpr.discharge -> locality val enforce_locality : bool option -> bool (** For commands whose default is to not discharge but to export: |