diff options
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 36 |
1 files changed, 16 insertions, 20 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 5edb7b808..7e470e844 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -132,10 +132,7 @@ GEXTEND Gram closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; Constr.ident: - [ [ id = Prim.ident -> id - - (* This is used in quotations and Syntax *) - | id = METAIDENT -> Id.of_string id ] ] + [ [ id = Prim.ident -> id ] ] ; Prim.name: [ [ "_" -> (!@loc, Anonymous) ] ] @@ -218,16 +215,13 @@ GEXTEND Gram CGeneralization (!@loc, Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> CGeneralization (!@loc, Explicit, None, c) - | "ltac:"; "("; tac = Tactic.tactic_expr; ")" -> + | IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in CHole (!@loc, None, IntroAnonymous, Some arg) ] ] ; record_declaration: - [ [ fs = record_fields -> CRecord (!@loc, None, fs) -(* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *) -(* CRecord (!@loc, Some c, fs) *) - ] ] + [ [ fs = record_fields -> CRecord (!@loc, fs) ] ] ; record_fields: @@ -267,14 +261,14 @@ GEXTEND Gram CLetTuple (!@loc,lb,po,c1,c2) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - CCases (!@loc, LetPatternStyle, None, [(c1,(None,None))], [(!@loc, [(!@loc,[p])], c2)]) + CCases (!@loc, LetPatternStyle, None, [c1, None, None], [(!@loc, [(!@loc,[p])], c2)]) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(!@loc, [(!@loc, [p])], c2)]) + CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [(!@loc, [(!@loc, [p])], c2)]) | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(!@loc, [(!@loc, [p])], c2)]) + CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [(!@loc, [(!@loc, [p])], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> @@ -338,11 +332,10 @@ GEXTEND Gram br=branches; "end" -> CCases(!@loc,RegularStyle,ty,ci,br) ] ] ; case_item: - [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ] - ; - pred_pattern: - [ [ ona = OPT ["as"; id=name -> id]; - ty = OPT ["in"; t=pattern -> t] -> (ona,ty) ] ] + [ [ c=operconstr LEVEL "100"; + ona = OPT ["as"; id=name -> id]; + ty = OPT ["in"; t=pattern -> t] -> + (c,ona,ty) ] ] ; case_type: [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ] @@ -386,14 +379,17 @@ GEXTEND Gram | "10" RIGHTA [ p = pattern; lp = LIST1 NEXT -> (match p with - | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp) + | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp) + | CPatCstr (_, r, None, l2) -> Errors.user_err_loc + (cases_pattern_expr_loc p, "compound_pattern", + Pp.str "Nested applications not supported.") | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp) | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp) | _ -> Errors.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Such pattern cannot have arguments.")) - |"@"; r = Prim.reference; lp = LIST1 NEXT -> - CPatCstr (!@loc, r, lp, []) ] + |"@"; r = Prim.reference; lp = LIST0 NEXT -> + CPatCstr (!@loc, r, Some lp, []) ] | "1" LEFTA [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ] | "0" |