From a4cc4ea007b074009bea485e75f7efef3d4d25f3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 28 Dec 2015 15:42:16 +0100
Subject: Removing unused parsing entries.

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

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 1fe12ce3e0..a7b05dd5eb 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -453,15 +453,6 @@ GEXTEND Gram
     [ [ check_for_coloneq; "(";  id = ident; bl = LIST0 simple_binder;
         ":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ]
   ;
-  hintbases:
-    [ [ "with"; "*" -> None
-      | "with"; l = LIST1 [ x = IDENT -> x] -> Some l
-      | -> Some [] ] ]
-  ;
-  auto_using:
-    [ [ "using"; l = LIST1 constr SEP "," -> l
-      | -> [] ] ]
-  ;
   eliminator:
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
-- 
cgit v1.2.3