From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 parsing/g_ltac.ml4 | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

(limited to 'parsing/g_ltac.ml4')

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;
-- 
cgit v1.2.3