diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
| tree | 591e9e512063e34099782e2518573f15ffeac003 /parsing/g_constr.ml4 | |
| parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) | |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index a1c0c9ae..130c6804 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_constr.ml4 9043 2006-07-12 10:06:40Z herbelin $ *) +(* $Id: g_constr.ml4 9226 2006-10-09 16:11:01Z herbelin $ *) open Pcoq open Constr @@ -155,8 +155,14 @@ GEXTEND Gram [ "200" RIGHTA [ c = binder_constr -> c ] | "100" RIGHTA - [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1, CastConv DEFAULTcast,c2) - | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,CastConv DEFAULTcast,c2) ] + [ c1 = operconstr; "<:"; c2 = binder_constr -> + CCast(loc,c1, CastConv VMcast,c2) + | c1 = operconstr; "<:"; c2 = SELF -> + CCast(loc,c1, CastConv VMcast,c2) + | c1 = operconstr; ":";c2 = binder_constr -> + CCast(loc,c1, CastConv DEFAULTcast,c2) + | c1 = operconstr; ":"; c2 = SELF -> + CCast(loc,c1, CastConv DEFAULTcast,c2) ] | "99" RIGHTA [ ] | "90" RIGHTA [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2) @@ -287,7 +293,7 @@ GEXTEND Gram (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) | _ -> Util.user_err_loc - (cases_pattern_loc p, "compound_pattern", + (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Constructor expected")) | p = pattern; "as"; id = ident -> CPatAlias (loc, p, id) ] |