diff options
| -rw-r--r-- | parsing/g_constrnew.ml4 | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index 3fc3e704e..e07e06b87 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -257,10 +257,9 @@ GEXTEND Gram ; case_item: [ [ c=operconstr LEVEL "100"; p=pred_pattern -> - match c,p with - | CRef (Ident (_,id)), (None,indp) -> (c,(Name id,indp)) - | _, (None,indp) -> (c,(Anonymous,indp)) - | _, (Some na,indp) -> (c,(na,indp)) ] ] + match p with + | (None,indp) -> (c,(Anonymous,indp)) + | (Some na,indp) -> (c,(na,indp)) ] ] ; pred_pattern: [ [ ona = OPT ["as"; id=name -> snd id]; |