diff options
| author | Maxime Dénès | 2018-02-21 19:02:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-21 19:02:56 +0100 |
| commit | 4b0fe4e09d547f0e6ee98da3fd6f7a134e51f3fd (patch) | |
| tree | 9550d5b99c9023c9c0ad84d2d7b89e05f344348b /parsing/g_constr.ml4 | |
| parent | 2f13806f10b2781f84417014c8018097c8e8b2ad (diff) | |
| parent | 2aff5c40ba9b40b4e0188b799dde6f31585e356b (diff) | |
Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 22 |
1 files changed, 7 insertions, 15 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index db68a75e09..9f12db649b 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -120,7 +120,7 @@ let name_colon = | _ -> err ()) | _ -> err ()) -let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None +let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family @@ -216,9 +216,11 @@ GEXTEND Gram | "("; c = operconstr LEVEL "200"; ")" -> (match c.CAst.v with | CPrim (Numeral (n,true)) -> - CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[])) + CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[],[])) | _ -> c) | "{|"; c = record_declaration; "|}" -> c + | "{"; c = binder_constr ; "}" -> + CAst.make ~loc:(!@loc) @@ CNotation(("{ _ }"),([c],[],[],[])) | "`{"; c = operconstr LEVEL "200"; "}" -> CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> @@ -385,19 +387,9 @@ GEXTEND Gram | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA - [ p = pattern; "as"; id = ident -> - CAst.make ~loc:!@loc @@ CPatAlias (p, id) - | p = pattern; lp = LIST1 NEXT -> - (let open CAst in match p with - | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp) - | { v = CPatCstr (r, None, l2); loc } -> - CErrors.user_err ?loc ~hdr:"compound_pattern" - (Pp.str "Nested applications not supported.") - | { v = CPatCstr (r, l1, l2) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp) - | { v = CPatNotation (n, s, l) } -> CAst.make ~loc:!@loc @@ CPatNotation (n , s, l@lp) - | _ -> CErrors.user_err - ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern" - (Pp.str "Such pattern cannot have arguments.")) + [ p = pattern; "as"; na = name -> + CAst.make ~loc:!@loc @@ CPatAlias (p, na) + | p = pattern; lp = LIST1 NEXT -> mkAppPattern ~loc:!@loc p lp | "@"; r = Prim.reference; lp = LIST0 NEXT -> CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ] | "1" LEFTA |