diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-17 00:00:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-17 00:00:41 +0000 |
| commit | 0cbcf76dc9ffa1f71c6aa5a8f255c9a3225163cc (patch) | |
| tree | f063008bdc359c49f486b1eeda71e6b04e3c556a /parsing/extend.ml | |
| 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.ml')
| -rw-r--r-- | parsing/extend.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml index 89a3da95f..0fd620e3c 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -33,6 +33,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 @@ -41,14 +42,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; @@ -236,10 +237,10 @@ let prod_item univ env = function | VTerm s -> env, Term (terminal s) | VNonTerm (loc, nt, Some p) -> let typ = nterm loc univ nt in - (p :: env, NonTerm (ProdPrimitive typ, Some (p,typ))) + (p :: env, NonTerm (typ, Some (p,typ))) | VNonTerm (loc, nt, None) -> let typ = nterm loc univ nt in - env, NonTerm (ProdPrimitive typ, None) + env, NonTerm (typ, None) let rec prod_item_list univ penv pil current_pos = match pil with @@ -256,7 +257,7 @@ let gram_rule univ (name,pil,act) = { gr_name = name; gr_production = pilc; gr_action = a } let border = function - | NonTerm (ProdPrimitive (ETConstr(_,BorderProd (_,a))),_) :: _ -> a + | NonTerm (ETConstr(_,BorderProd (_,a)),_) :: _ -> a | _ -> None let clever_assoc ass g = |