aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_constrnew.ml44
1 files changed, 1 insertions, 3 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index c3a7c27b3a..e8f9c38c5e 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -287,9 +287,7 @@ GEXTEND Gram
;
pred_pattern:
[ [ oid = ["as"; id=name -> snd id | -> Names.Anonymous];
- ty = OPT ["in"; r=global; nal=LIST0 name ->
- (loc,r,List.map snd nal)] ->
- (oid,ty) ] ]
+ ty = OPT ["in"; t=lconstr -> t] -> (oid,ty) ] ]
;
case_type:
[ [ ty = OPT [ "return"; c = operconstr LEVEL "100" -> c ] -> ty ] ]