From b774a857b1ef8d123daf05f0a57393844c078369 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 17 Nov 2002 00:11:45 +0000
Subject: 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
---
 parsing/egrammar.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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)
 
-- 
cgit v1.2.3