summaryrefslogtreecommitdiff
path: root/parsing/g_constrnew.ml4
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-01-19 22:34:29 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-01-19 22:34:29 +0000
commit018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (patch)
treefbb91e2f74c73bb867ab62c58f248a704bbe6dec /parsing/g_constrnew.ml4
parent6497f27021fec4e01f2182014f2bb1989b4707f9 (diff)
Imported Upstream version 8.0pl3upstream/8.0pl3
Diffstat (limited to 'parsing/g_constrnew.ml4')
-rw-r--r--parsing/g_constrnew.ml46
1 files changed, 4 insertions, 2 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index adc26532..fe579e98 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_constrnew.ml4,v 1.41.2.2 2004/11/17 12:48:35 herbelin Exp $ *)
+(* $Id: g_constrnew.ml4,v 1.41.2.4 2005/09/21 14:47:33 herbelin Exp $ *)
open Pcoq
open Constr
@@ -285,7 +285,9 @@ GEXTEND Gram
[ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
;
pattern:
- [ "10" LEFTA
+ [ "200" RIGHTA [ ]
+ | "99" RIGHTA [ ]
+ | "10" LEFTA
[ p = pattern ; lp = LIST1 (pattern LEVEL "0") ->
(match p with
| CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)