diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-31 08:52:24 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-31 08:52:24 +0000 |
| commit | fd6ad12c8a80dbac5bc1cb3d7735e3543d8d01b8 (patch) | |
| tree | 75c38585ef773678d88881c55342ad5348dee955 /parsing | |
| parent | 71a48bb529cbaa36bc53b2ec3b721235b2b2ec38 (diff) | |
assouplissement de la syntaxe du let de ltac: t1 ; let in autorise
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9324 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 24 |
1 files changed, 15 insertions, 9 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index cd447e537..33268f29c 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -47,16 +47,10 @@ GEXTEND Gram tactic_expr: [ "5" RIGHTA - [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr -> - TacFun (it,body) - | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in"; - body = tactic_expr -> TacLetRecIn (rcl,body) - | "let"; llc = LIST1 let_clause SEP "with"; "in"; - u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u) - | IDENT "info"; tc = tactic_expr -> TacInfo tc ] - + [ te = binder_tactic -> te ] | "4" LEFTA [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1) + | ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1) | ta = tactic_expr; ";"; "["; lta = LIST0 OPT tactic_expr SEP "|"; "]" -> let lta = List.map (function None -> TacId [] | Some t -> t) lta in @@ -72,7 +66,8 @@ GEXTEND Gram TacAbstract (tc,Some s) ] (*End of To do*) | "2" RIGHTA - [ ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] + [ ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) + | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) ] | "1" RIGHTA [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> TacMatchContext (b,false,mrl) @@ -104,6 +99,17 @@ GEXTEND Gram [ "("; a = tactic_expr; ")" -> a | a = tactic_atom -> TacArg a ] ] ; + (* binder_tactic: level 5 of tactic_expr *) + binder_tactic: + [ RIGHTA + [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> + TacFun (it,body) + | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in"; + body = tactic_expr LEVEL "5" -> TacLetRecIn (rcl,body) + | "let"; llc = LIST1 let_clause SEP "with"; "in"; + u = tactic_expr LEVEL "5" -> TacLetIn (make_letin_clause loc llc,u) + | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ] + ; (* Tactic arguments *) tactic_arg: [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> tacarg_of_expr a |