diff options
| author | Pierre-Marie Pédrot | 2020-10-29 13:59:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-21 13:55:32 +0100 |
| commit | 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 (patch) | |
| tree | 9913737179ee72e0c1b9672227fe5872ce6734a9 /vernac/vernacentries.ml | |
| parent | a714abe0a1c0cac277297f9e3c7f6d90ac0173d6 (diff) | |
Move evaluable_global_reference from Names to Tacred.
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a3726daf63..e8cb1d65a9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1628,6 +1628,7 @@ let () = } let vernac_set_strategy ~local l = + let open Tacred in let local = Option.default false local in let glob_ref r = match smart_global r with @@ -1639,6 +1640,7 @@ let vernac_set_strategy ~local l = Redexpr.set_strategy local l let vernac_set_opacity ~local (v,l) = + let open Tacred in let local = Option.default true local in let glob_ref r = match smart_global r with |