diff options
| -rw-r--r-- | parsing/argextend.ml4 | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 34ed304764..21f5a7368c 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -267,11 +267,14 @@ EXTEND declare_vernac_argument false loc s l ] ] ; argtype: - [ [ e = LIDENT -> fst (interp_entry_name loc e) - | e1 = LIDENT; "*"; e2 = LIDENT -> - let e1 = fst (interp_entry_name loc e1) in - let e2 = fst (interp_entry_name loc e2) in - PairArgType (e1, e2) ] ] + [ "2" + [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ] + | "1" + [ e = argtype; LIDENT "list" -> List0ArgType e + | e = argtype; LIDENT "option" -> OptArgType e ] + | "0" + [ e = LIDENT -> fst (interp_entry_name loc e) + | "("; e = argtype; ")" -> e ] ] ; argrule: [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ] |