diff options
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 1fe12ce3e..a7b05dd5e 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 ] ] ; |