diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-15 22:30:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-16 12:17:39 +0200 |
| commit | cd3971e53b76cb62e14822eb3e275d3968a4f215 (patch) | |
| tree | dc2bdaa617d1bd30209ae63083c9e4d7d392917d /plugins/ltac/g_ltac.ml4 | |
| parent | 9f8220164703aee47c6c6d7dba07caabf7555c1c (diff) | |
Adding support for using grammar entries returning no value in EXTEND.
Diffstat (limited to 'plugins/ltac/g_ltac.ml4')
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ca5d198c2..d717ed0a5 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -460,7 +460,9 @@ END let pr_ltac_production_item = function | Tacentries.TacTerm s -> quote (str s) -| Tacentries.TacNonTerm (_, (arg, sep), id) -> +| Tacentries.TacNonTerm (_, (arg, None), None) -> str arg +| Tacentries.TacNonTerm (_, (arg, Some _), None) -> assert false +| Tacentries.TacNonTerm (_, (arg, sep), Some id) -> let sep = match sep with | None -> mt () | Some sep -> str "," ++ spc () ++ quote (str sep) @@ -470,7 +472,9 @@ let pr_ltac_production_item = function VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item | [ string(s) ] -> [ Tacentries.TacTerm s ] | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> - [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), p) ] + [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), Some p) ] +| [ ident(nt) ] -> + [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, None), None) ] END VERNAC COMMAND EXTEND VernacTacticNotation |