diff options
| author | Pierre-Marie Pédrot | 2016-02-29 12:40:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-29 13:24:45 +0100 |
| commit | 293222e49ff81bc1299b3822d2a8c526ca803307 (patch) | |
| tree | fff87b81ee563870658be00b3686e70d3262cf59 /printing | |
| parent | ae3bbff3ca2564fe24bdf3dd517c82807eae9151 (diff) | |
Moving the "exists" tactic to TACTIC EXTEND.
Diffstat (limited to 'printing')
| -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 ( |