diff options
| author | Jim Fehrle | 2019-10-30 14:57:57 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-10-30 14:57:57 -0700 |
| commit | 2e04ae60563534fc6f339149051d2d8c09d7a69a (patch) | |
| tree | bb2ab1a4d5723b8a1b70215dff9f18f3b0b177e4 /parsing | |
| parent | 28ea499486dd17076d8f2f4c31d7fdebeacdff8e (diff) | |
Rename the 2 local type_cstr nonterminals to give them unique names
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.mlg | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 87b9a8eea3..470782a7dc 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -263,7 +263,7 @@ GRAMMAR EXTEND Gram { mkProdCN ~loc bl c } | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> { mkLambdaCN ~loc bl c } - | "let"; id=name; bl = binders; ty = type_cstr; ":="; + | "let"; id=name; bl = binders; ty = let_type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> { let ty,c1 = match ty, c1 with | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *) @@ -353,7 +353,7 @@ GRAMMAR EXTEND Gram | "cofix" -> { false } ] ] ; fix_decl: - [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":="; + [ [ id=identref; bl=binders_fixannot; ty=let_type_cstr; ":="; c=operconstr LEVEL "200" -> { (id,fst bl,snd bl,c,ty) } ] ] ; @@ -525,7 +525,7 @@ GRAMMAR EXTEND Gram ] ] ; - type_cstr: + let_type_cstr: [ [ c=OPT [":"; c=lconstr -> { c } ] -> { Loc.tag ~loc c } ] ] ; END |