diff options
| author | herbelin | 2002-11-17 00:11:45 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-17 00:11:45 +0000 |
| commit | b774a857b1ef8d123daf05f0a57393844c078369 (patch) | |
| tree | 3b46fb8fa2154ce989460644e5a4fb1bb66577a0 | |
| parent | ab4f34c860fcd5b5362ea96097fbd51fbbf3f99a (diff) | |
Problème avec le choix d'introduire une indirection vers un rawconstr pour
les extensions de grammaire par Grammar; pose p.ex. problème pour la
résolution des implicites. Pour l'instant, une rustine pour contourner
le problème
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3248 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/egrammar.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index cec7e44586..33ca1214fc 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -137,7 +137,13 @@ let make_rule univ etyp rule = let make_rule univ etyp rule = let pil = List.map (symbol_of_prod_item univ) rule.gr_production in let (symbs,ntl) = List.split pil in - let f loc env = CGrammar (loc, rule.gr_action, env) in + let f loc env = match rule.gr_action, env with + | AVar p, [p',a] when p=p' -> a + | AApp (AVar f,[AVar a]), [f',v;a',w] when f=f' & a=a' -> + CApp (loc,v,[w,None]) + | AApp (AVar f,[AVar a]), [a',w;f',v] when f=f' & a=a' -> + CApp (loc,v,[w,None]) + | pat,_ -> CGrammar (loc, pat, env) in let act = make_act f ntl in (symbs, act) |