diff options
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 |