diff options
| author | herbelin | 2004-03-17 00:00:41 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-17 00:00:41 +0000 |
| commit | 0cbcf76dc9ffa1f71c6aa5a8f255c9a3225163cc (patch) | |
| tree | f063008bdc359c49f486b1eeda71e6b04e3c556a /parsing/extend.mli | |
| parent | e607a6c08a011f66716969215ddb0e7776e86c60 (diff) | |
Mise en place de motifs récursifs dans Notation; quelques simplifications au passage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5510 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/extend.mli')
| -rw-r--r-- | parsing/extend.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/parsing/extend.mli b/parsing/extend.mli index 4aae3e3094..a95f1134b0 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -34,6 +34,7 @@ type ('lev,'pos) constr_entry_key = | ETConstr of ('lev * 'pos) | ETPattern | ETOther of string * string + | ETConstrList of ('lev * 'pos) * Token.pattern list type constr_production_entry = (production_level,production_position) constr_entry_key @@ -42,14 +43,14 @@ type simple_constr_production_entry = (production_level,unit) constr_entry_key type nonterm_prod = | ProdList0 of nonterm_prod - | ProdList1 of nonterm_prod + | ProdList1 of nonterm_prod * Token.pattern list | ProdOpt of nonterm_prod | ProdPrimitive of constr_production_entry type prod_item = | Term of Token.pattern - | NonTerm of - nonterm_prod * (Names.identifier * constr_production_entry) option + | NonTerm of constr_production_entry * + (Names.identifier * constr_production_entry) option type grammar_rule = { gr_name : string; |