diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-07-18 00:33:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-07-18 00:33:02 +0200 |
| commit | ddf50c8bb15ce86fc3e3fbedf9f86fd278f01776 (patch) | |
| tree | fae5b58556a6d27a7d6b93890f723a29f0fcc486 /parsing | |
| parent | a622696bbe5c6752e49dabb4d3740acf113080ee (diff) | |
Removing useless grammar entries. Fixes bug #4919.
Diffstat (limited to 'parsing')
| -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 *) |