diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-28 15:42:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-28 15:42:16 +0100 |
| commit | a4cc4ea007b074009bea485e75f7efef3d4d25f3 (patch) | |
| tree | 9a0cc9b250c44a30f0fa96d0f2cf088445a4187e /parsing/g_tactic.ml4 | |
| parent | 9af1d5ae4dbed8557b5c715a65f2742c57641f52 (diff) | |
Removing unused parsing entries.
Diffstat (limited to 'parsing/g_tactic.ml4')
| -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 ] ] ; |