diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 689ac6e4eb..2c57cb811e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -725,7 +725,6 @@ module Make (* some shortcuts *) let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in - let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in let pr_with_bindings_arg_full = pr_with_bindings_arg in let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in @@ -909,13 +908,6 @@ module Make l ) - (* Constructors *) - | TacSplit (ev,l) -> - hov 1 ( - primitive (with_evars ev "exists") - ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l - ) - (* Conversion *) | TacReduce (r,h) -> hov 1 ( |