diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-15 17:10:02 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-15 17:10:02 +0000 |
| commit | 961c655f62d012c16371643f9c639027b7150820 (patch) | |
| tree | e8d22cc2c419f56c8ba049c63b9fa6dfddd2a975 /parsing | |
| parent | f929791a2ce1c74ac28a832bfe48ff07821f096f (diff) | |
Egramml: minor simplification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15890 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramml.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 735a31f21..ae7351a9a 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -26,11 +26,6 @@ let make_generic_action Gram.action (fun v -> make ((p,in_generic t v) :: env) tl) in make [] (List.rev pil) -let make_rule_gen mkproditem mkact pt = - let (symbs,ntl) = List.split (List.map mkproditem pt) in - let act = make_generic_action mkact ntl in - (symbs, act) - (** Grammar extensions declared at ML level *) type grammar_prod_item = @@ -43,7 +38,10 @@ let make_prod_item = function | GramNonTerminal (_,t,e,po) -> (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po) -let make_rule mkact = make_rule_gen make_prod_item mkact +let make_rule mkact pt = + let (symbs,ntl) = List.split (List.map make_prod_item pt) in + let act = make_generic_action mkact ntl in + (symbs, act) (** Tactic grammar extensions *) |