Removing unused parsing entries.

1 files changed, 0 insertions, 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 ] ]
   ;