diff options
| author | herbelin | 2004-06-17 13:52:14 +0000 |
|---|---|---|
| committer | herbelin | 2004-06-17 13:52:14 +0000 |
| commit | c22fe3fa533e219037e453eaeebbc279bf4a9909 (patch) | |
| tree | 1ff7051e4d33f9c2b0b9781081a51549b07d38d6 | |
| parent | f8b4a0db07bb2d82fb07696ca3a7d933ab1a8448 (diff) | |
Nouvelle syntaxe à la ML pour donner le type ML des extensions d'arguments
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5815 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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) ] ] |