diff options
| author | Pierre-Marie Pédrot | 2016-03-20 16:34:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 16:34:56 +0100 |
| commit | 1890a2cdc0dcda7335d7f81fc9ce77c0debc4324 (patch) | |
| tree | 92ef47814ba09193cac2cff57084dbb8fa9b739a | |
| parent | 25bbce0e0cb841a7ad9d5c3e7ce33711b27bf41b (diff) | |
Fixing the classification of Tactic Notation.
| -rw-r--r-- | tactics/g_ltac.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4 index f46a670080..b55ac9ad06 100644 --- a/tactics/g_ltac.ml4 +++ b/tactics/g_ltac.ml4 @@ -398,8 +398,9 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item [ TacNonTerm (loc, Names.Id.to_string nt, (p, Option.default "" sep)) ] END -VERNAC COMMAND EXTEND VernacTacticNotation CLASSIFIED AS SIDEFF -| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] -> +VERNAC COMMAND EXTEND VernacTacticNotation +| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => + [ VtUnknown, VtNow ] -> [ let l = Locality.LocalityFixme.consume () in let n = Option.default 0 n in |