diff options
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) -> |