diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-01 11:20:52 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-01 11:41:21 +0200 |
| commit | 88d5621e0d70482e5869e9b422ff30b14f58691a (patch) | |
| tree | a75a129b4de6f37b58bc1f89a79f1991d06e3dd0 /parsing | |
| parent | bf5763c6d871d70a4629f378d138ffbf26b765d6 (diff) | |
g_tactics : remove opt_bindings (2-line dead code)
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 87e27be69..cfe5377d6 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -338,9 +338,6 @@ GEXTEND Gram ExplicitBindings bl | bl = LIST1 constr -> ImplicitBindings bl ] ] ; - opt_bindings: - [ [ bl = LIST1 bindings SEP "," -> bl | -> [NoBindings] ] ] - ; constr_with_bindings: [ [ c = constr; l = with_bindings -> (c, l) ] ] ; |