From 05dffdc0a9c3a3ba62a9756f5b33e7182e818656 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Dec 2002 10:35:41 +0000
Subject: Prise en compte notations dans les extensions de motiff

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3484 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/egrammar.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 67aacdd567..192f84d6be 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -285,6 +285,8 @@ let make_rule univ assoc etyp rule =
         (* Ugly *)
         let f loc env = match rule.gr_action, env with
           | CRef (Ident(_,p)), [p',a] when p=p' -> a
+          | CDelimiters (_,s,CRef (Ident(_,p))), [p',a] when p=p' ->
+	      CPatDelimiters (loc,s,a)
           | _ -> error "Unable to handle this grammar extension of pattern" in
 	make_cases_pattern_act f ntl
     | ETIdent | ETBigint | ETReference -> error "Cannot extend"
-- 
cgit v1.2.3