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 /printing/pptactic.ml | |
| parent | bf18afeefa06e972c6cb98fa8a81ec7172fdde7f (diff) | |
Moving left & right tactics out of the AST.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index a5b07c4770..587a8db41b 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -766,8 +766,6 @@ and pr_atom1 = function hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l) (* Constructors *) - | TacLeft (ev,l) -> hov 1 (str (with_evars ev "left") ++ pr_bindings l) - | TacRight (ev,l) -> hov 1 (str (with_evars ev "right") ++ pr_bindings l) | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ prlist_with_sep pr_comma pr_bindings l) | TacSplit (ev,true,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l) | TacAnyConstructor (ev,Some t) -> |