diff options
| author | Emilio Jesus Gallego Arias | 2017-11-20 15:42:18 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-22 22:48:00 +0100 |
| commit | 57f62f06419972ba799e451d2f56552dc1b2fb63 (patch) | |
| tree | 6bd9d8b3f6f8a2f6bd0201ea8ebcc414fa38db6d /plugins/ltac/g_auto.ml4 | |
| parent | ce418aea93a6396412de57aded0ff092bec7596b (diff) | |
[plugin] Remove LocalityFixme über hack.
To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.
This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.
Diffstat (limited to 'plugins/ltac/g_auto.ml4')
| -rw-r--r-- | plugins/ltac/g_auto.ml4 | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 84e79d8abd..90a44708fc 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -190,7 +190,7 @@ END let pr_hints_path prc prx pry c = Hints.pp_hints_path c let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c let glob_hints_path ist = Hints.glob_hints_path - + ARGUMENT EXTEND hints_path PRINTED BY pr_hints_path @@ -214,10 +214,15 @@ ARGUMENT EXTEND opthints | [ ] -> [ None ] END -VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ - let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (match dbnames with None -> ["core"] | Some l -> l) entry ] + fun ~atts ~st -> begin + let open Vernacinterp in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in + Hints.add_hints (Locality.make_section_locality atts.locality) + (match dbnames with None -> ["core"] | Some l -> l) entry; + st + end + ] END |