diff options
| author | herbelin | 2000-11-20 08:52:28 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-20 08:52:28 +0000 |
| commit | b7e5541cd7b04f331b8939b069b217029e11f00b (patch) | |
| tree | fd80ab2c0102e3e4ec8eaf8c1fcf71cd38e57484 | |
| parent | 6f42f7349bb74cebbf01b7a9ca084cac478b8e6d (diff) | |
Acceptation des noms qualifiés; nouveau lexeme METAIDENT pour les $id
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@879 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_constr.ml4 | 30 |
1 files changed, 24 insertions, 6 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index c7ab5fb855..e4cbc2c1da 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -9,10 +9,27 @@ open Constr GEXTEND Gram GLOBAL: ident constr0 constr1 constr2 constr3 lassoc_constr4 constr5 constr6 constr7 constr8 constr9 constr10 lconstr constr - ne_ident_comma_list ne_constr_list sort ne_binders_list; - + ne_ident_comma_list ne_constr_list sort ne_binders_list qualid + global; ident: - [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ] + [ [ id = IDENT -> <:ast< ($VAR $id) >> + + (* This is used in quotations *) + | id = METAIDENT -> <:ast< ($VAR $id) >> ] ] + ; + global: + [ [ l = qualid -> <:ast< (QUALID ($LIST l)) >> + + (* This is used in quotations *) + | id = METAIDENT -> <:ast< ($VAR $id) >> ] ] + ; + qualid: + [ [ id = IDENT; l = fields -> <:ast< ($VAR $id) >> :: l ] ] + ; + fields: + [ [ id = FIELD; l = fields -> <:ast< ($VAR $id) >> :: l + | -> [] + ] ] ; raw_constr: [ [ c = Prim.ast -> c ] ] @@ -61,7 +78,8 @@ GEXTEND Gram | IDENT "CoFix"; id = ident; "{"; fbinders = cofixbinders; "}" -> <:ast< (COFIX $id ($LIST $fbinders)) >> | s = sort -> s - | v = ident -> v ] ] + | v = global -> v + ] ] ; constr1: [ [ "<"; ":"; IDENT "ast"; ":"; "<"; c = raw_constr; ">>" -> c @@ -129,8 +147,8 @@ GEXTEND Gram | c1 = constr8; "::"; c2 = constr8 -> <:ast< (CAST $c1 $c2) >> ] ] ; constr10: - [ [ "!"; f = IDENT; args = ne_constr9_list -> - <:ast< (APPLISTEXPL ($VAR $f) ($LIST $args)) >> + [ [ "!"; f = global; args = ne_constr9_list -> + <:ast< (APPLISTEXPL $f ($LIST $args)) >> | f = constr9; args = ne_constr91_list -> <:ast< (APPLIST $f ($LIST $args)) >> | f = constr9 -> f ] ] |