diff options
Diffstat (limited to 'parsing/g_ltac.ml4')
| -rw-r--r-- | parsing/g_ltac.ml4 | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index dbd81e7f..316bf8e1 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_ltac.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: g_ltac.ml4 11576 2008-11-10 19:13:15Z msozeau $ *) open Pp open Util @@ -165,11 +165,24 @@ GEXTEND Gram match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - Subterm (oid, pc) + Subterm (false,oid, pc) + | IDENT "appcontext"; oid = OPT Constr.ident; + "["; pc = Constr.lconstr_pattern; "]" -> + Subterm (true,oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: - [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) ] ] + [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) + | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt) + | na = name; ":="; mpv = match_pattern -> + let t, ty = + match mpv with + | Term t -> (match t with + | CCast (loc, t, CastConv (_, ty)) -> Term t, Some (Term ty) + | _ -> mpv, None) + | _ -> mpv, None + in Def (na, t, Option.default (Term (CHole (dummy_loc, None))) ty) + ] ] ; match_context_rule: [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; |