summaryrefslogtreecommitdiff
path: root/parsing/g_ltac.ml4
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /parsing/g_ltac.ml4
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'parsing/g_ltac.ml4')
-rw-r--r--parsing/g_ltac.ml419
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;