diff options
Diffstat (limited to 'parsing/g_cases.ml4')
| -rw-r--r-- | parsing/g_cases.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4 index 62ee20cad..679d174c2 100644 --- a/parsing/g_cases.ml4 +++ b/parsing/g_cases.ml4 @@ -20,7 +20,7 @@ let pair loc = Qualid (loc, Libnames.qualid_of_string "Coq.Init.Datatypes.pair") GEXTEND Gram - GLOBAL: constr pattern; + GLOBAL: operconstr pattern; pattern: [ [ r = Prim.reference -> CPatAtom (loc,Some r) @@ -47,12 +47,12 @@ GEXTEND Gram | p = pattern -> p ] ] ; equation: - [ [ lhs = LIST1 pattern; "=>"; rhs = constr9 -> (loc,lhs,rhs) ] ] + [ [ lhs = LIST1 pattern; "=>"; rhs = operconstr LEVEL "9" -> (loc,lhs,rhs) ] ] ; ne_eqn_list: [ [ leqn = LIST1 equation SEP "|" -> leqn ] ] ; - constr: LEVEL "1" + operconstr: LEVEL "1" [ [ "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of"; OPT "|"; eqs = ne_eqn_list; "end" -> CCases (loc, Some p, lc, eqs) |