From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- parsing/g_cases.ml4 | 73 ----------------------------------------------------- 1 file changed, 73 deletions(-) delete mode 100644 parsing/g_cases.ml4 (limited to 'parsing/g_cases.ml4') diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4 deleted file mode 100644 index b952305d..00000000 --- a/parsing/g_cases.ml4 +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* CPatAtom (loc,Some r) - | IDENT "_" -> CPatAtom (loc,None) - (* Hack to parse syntax "(n)" as a natural number *) - | "("; G_constr.test_int_rparen; n = bigint; ")" -> - (* Delimiter "N" moved to "nat" in V7 *) - CPatDelimiters (loc,"nat",CPatNumeral (loc,n)) - | "("; p = compound_pattern; ")" -> p - | n = bigint -> CPatNumeral (loc,n) - | "'"; G_constr.test_ident_colon; key = IDENT; ":"; c = pattern; "'" -> - CPatDelimiters (loc,key,c) - ] ] - ; - compound_pattern: - [ [ p = pattern ; lp = LIST1 pattern -> - (match p with - | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) - | _ -> Util.user_err_loc - (loc, "compound_pattern", Pp.str "Constructor expected")) - | p = pattern; "as"; id = base_ident -> - CPatAlias (loc, p, id) - | p1 = pattern; ","; p2 = pattern -> - CPatCstr (loc, pair loc, [p1; p2]) - | p = pattern -> p ] ] - ; - equation: - [ [ lhs = LIST1 pattern; "=>"; rhs = operconstr LEVEL "9" -> (loc,lhs,rhs) ] ] - ; - ne_eqn_list: - [ [ leqn = LIST1 equation SEP "|" -> leqn ] ] - ; - operconstr: LEVEL "1" - [ [ "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of"; - OPT "|"; eqs = ne_eqn_list; "end" -> - let lc = List.map (fun c -> c,(None,None)) lc in - CCases (loc, (Some p,None), lc, eqs) - | "Cases"; lc = LIST1 constr; "of"; - OPT "|"; eqs = ne_eqn_list; "end" -> - let lc = List.map (fun c -> c,(None,None)) lc in - CCases (loc, (None,None), lc, eqs) - | "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of"; "end" -> - let lc = List.map (fun c -> c,(None,None)) lc in - CCases (loc, (Some p,None), lc, []) - | "Cases"; lc = LIST1 constr; "of"; "end" -> - let lc = List.map (fun c -> c,(None,None)) lc in - CCases (loc, (None,None), lc, []) ] ] - ; -END; -- cgit v1.2.3