aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_tactic.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_tactic.ml4')
-rw-r--r--parsing/g_tactic.ml49
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 *)