diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-24 17:24:46 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-24 17:41:21 +0200 |
| commit | 6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 (patch) | |
| tree | b8a60ea2387f14a415d53a3cd9db516e384a5b4f /plugins/ltac/g_ltac.ml4 | |
| parent | a02f76f38592fd84cabd34102d38412f046f0d1b (diff) | |
| parent | 28f8da9489463b166391416de86420c15976522f (diff) | |
Merge branch 'trunk' into located_switch
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 5fc22cb4a..b5028190f 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.tag ~loc ((Names.Id.to_string nt, sep), p)) ] + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), Some p)) ] +| [ ident(nt) ] -> + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, None), None)) ] END VERNAC COMMAND EXTEND VernacTacticNotation |