From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

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

(limited to 'parsing/g_ltac.ml4')

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 78a9fbc7..dbd81e7f 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 10919 2008-05-11 22:04:26Z msozeau $ *)
+(* $Id: g_ltac.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -72,10 +72,10 @@ GEXTEND Gram
       | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
     | "1" RIGHTA
       [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
-          TacMatchContext (b,false,mrl)
+          TacMatchGoal (b,false,mrl)
       | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
         mrl = match_context_list; "end" ->
-          TacMatchContext (b,true,mrl)
+          TacMatchGoal (b,true,mrl)
       |	b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
           TacMatch (b,c,mrl)
       | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
-- 
cgit v1.2.3