From ddf50c8bb15ce86fc3e3fbedf9f86fd278f01776 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 18 Jul 2016 00:33:02 +0200
Subject: Removing useless grammar entries. Fixes bug #4919.

---
 parsing/g_tactic.ml4 | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 8ecc7d015a..199ef9fcee 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 *)
-- 
cgit v1.2.3