diff options
| author | Pierre-Marie Pédrot | 2020-03-11 11:29:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-18 11:44:50 +0100 |
| commit | 245b94cd075b6be527590c425a98262d89577909 (patch) | |
| tree | 0e989e6db3f1e113cc0bb59c92f6e88424f92b79 /plugins | |
| parent | 693c0fb3ad7344aadc840ab7124782e64997b739 (diff) | |
Hack a non-superglobal mode for hints.
The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_auto.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 82c64a9857..336c5a4bb0 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -249,7 +249,7 @@ END VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF | #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints ~local:(Locality.make_section_locality locality) + Hints.add_hints ~local:(Locality.make_section_locality locality) ~superglobal:true (match dbnames with None -> ["core"] | Some l -> l) entry; } END |