diff options
Diffstat (limited to 'parsing/g_tactic.ml4')
-rw-r--r-- | parsing/g_tactic.ml4 | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 8ecc7d015..199ef9fce 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -490,9 +490,6 @@ GEXTEND Gram [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac | -> None ] ] ; - rename : - [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] - ; rewriter : [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c) | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c) @@ -518,12 +515,6 @@ GEXTEND Gram | _,_,Some _ -> err () | _,_,None -> (ic,el) ]] ; - move_location: - [ [ IDENT "after"; id = id_or_meta -> MoveAfter id - | IDENT "before"; id = id_or_meta -> MoveBefore id - | "at"; IDENT "top" -> MoveFirst - | "at"; IDENT "bottom" -> MoveLast ] ] - ; simple_tactic: [ [ (* Basic tactics *) |