diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-04-18 10:16:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-04-20 12:18:01 +0200 |
| commit | b846c413c2e79520a5238c5a0775f5cd73d61bac (patch) | |
| tree | 1292d6af5857ab3e3075d19ae99aedf045725555 | |
| parent | 738551a294d5d8393253568764f9bea4cf45f7c5 (diff) | |
Inlining "fun" and "forall" tokens in parser, so that alternative notations for
them (e.g. "fun ... ⇒ ...") factor well (see #2268).
| -rw-r--r-- | parsing/g_constr.ml4 | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 3bb029a88..74f17f9fb 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -223,12 +223,6 @@ GEXTEND Gram CHole (!@loc, None, IntroAnonymous, Some arg) ] ] ; - forall: - [ [ "forall" -> () ] ] - ; - lambda: - [ [ "fun" -> () ] ] - ; record_declaration: [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs) (* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *) @@ -240,9 +234,9 @@ GEXTEND Gram (id, abstract_constr_expr c (binders_of_lidents params)) ] ] ; binder_constr: - [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" -> + [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" -> mkCProdN (!@loc) bl c - | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> + | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> mkCLambdaN (!@loc) bl c | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> |