diff options
Diffstat (limited to 'parsing/g_ltac.ml4')
| -rw-r--r-- | parsing/g_ltac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
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 "|"; "]" -> |