diff options
| -rw-r--r-- | parsing/g_tactic.ml4 | 3 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index d396854ba7..f27191e2ec 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -155,7 +155,8 @@ GEXTEND Gram ; simple_intropattern: [ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc - | "("; tc = LIST1 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc] + | "("; tc = LIST0 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc] + | "()" -> IntroOrAndPattern [[]] | "_" -> IntroWildcard | id = ident -> IntroIdentifier id ] ] diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index c2029dde5b..46caf88b82 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -354,7 +354,7 @@ let rec pr_intro_pattern = function | IntroWildcard -> str "_" | IntroIdentifier id -> pr_id id and pr_case_intro_pattern = function - | [_::_ as pl] -> + | [pl] -> str "(" ++ hov 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")" | pll -> str "[" ++ |