diff options
| author | delahaye | 2001-04-20 08:11:23 +0000 |
|---|---|---|
| committer | delahaye | 2001-04-20 08:11:23 +0000 |
| commit | efbc16c17d5ff8d4db80213368b43ad10fe6c461 (patch) | |
| tree | 36f673fd59b02971eb61a745798008d3b218bebb | |
| parent | eeff794a56b9ece701932babf34a681a81d96d0b (diff) | |
Petit menage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1642 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_tactic.ml4 | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index d9a8e13189..e32a649f05 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -323,30 +323,6 @@ GEXTEND Gram -> <:ast< (MATCHCONTEXT ($LIST $mrl)) >> | IDENT "Match"; com = constrarg; IDENT "With"; mrl = match_list -> <:ast< (MATCH $com ($LIST $mrl)) >> - -(* | IDENT "First" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - <:ast<(FIRST ($LIST $l))>> - | IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - <:ast<(TCLSOLVE ($LIST $l))>> - | IDENT "Info"; tc = tactic_expr_par -> <:ast< (INFO $tc) >> - | IDENT "Try"; ta0 = tactic_expr_par; "Orelse"; ta1 = tactic_expr_par -> - <:ast< (TRY (ORELSE $ta0 $ta1)) >> - | IDENT "Try"; ta = tactic_expr_par -> <:ast< (TRY $ta) >> - | IDENT "Do"; n = pure_numarg; ta = tactic_expr_par -> - <:ast< (DO $n $ta) >> - | IDENT "Repeat"; ta = tactic_expr_par -> <:ast< (REPEAT $ta) >> - | IDENT "Repeat"; ta0 = tactic_expr_par; "Orelse"; - ta1 = tactic_expr_par -> - <:ast< (REPEAT (ORELSE $ta0 $ta1)) >> - | IDENT "Idtac" -> <:ast< (IDTAC) >> - | IDENT "Fail" -> <:ast<(FAIL)>> - | IDENT "Fail"; n = pure_numarg -> <:ast<(FAIL $n)>> - | st = simple_tactic -> st - | st = simple_tactic; "Orelse"; ta1 = tactic_expr_par -> - <:ast< (ORELSE $st $ta1) >> - | ta0 = tactic_expr_par; "Orelse"; ta1 = tactic_expr_par -> - <:ast< (ORELSE $ta0 $ta1) >>*) - | "("; te = tactic_expr; ")" -> te | "("; te = tactic_expr; tel=LIST1 tactic_expr; ")" -> <:ast< (APP $te ($LIST tel)) >> |