diff options
| author | Pierre-Marie Pédrot | 2014-05-21 17:08:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-21 17:38:48 +0200 |
| commit | 741747c4ecb2be5f51bf5e0395f9fcb28329e86b (patch) | |
| tree | 1c9595161bca3a6f2bf5f2503bb03b33b31c49f5 /parsing | |
| parent | bf18afeefa06e972c6cb98fa8a81ec7172fdde7f (diff) | |
Moving left & right tactics out of the AST.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 3e80c99f5a..5f9f6e472d 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -634,10 +634,6 @@ GEXTEND Gram | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l (* Constructors *) - | IDENT "left"; bl = with_bindings -> TacLeft (false,bl) - | IDENT "eleft"; bl = with_bindings -> TacLeft (true,bl) - | IDENT "right"; bl = with_bindings -> TacRight (false,bl) - | IDENT "eright"; bl = with_bindings -> TacRight (true,bl) | IDENT "split"; bl = with_bindings -> TacSplit (false,false,[bl]) | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,[bl]) | "exists"; bll = LIST1 opt_bindings SEP "," -> TacSplit (false,true,bll) |