diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-01 05:42:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-01 05:42:14 +0200 |
| commit | a0ea7ebf4838903c3ed9a9b885716cf14134a0c8 (patch) | |
| tree | 8a073c4a47c29d0f9b19aec6d28c0c62dbe8a3d5 /plugins/ltac/pptactic.mli | |
| parent | eed90d1bd867dce59f6bf1b2bf769fff188f128b (diff) | |
[printing] Remove duplicated printing function.
It seems there were 4 copies of the same function in the code base.
Diffstat (limited to 'plugins/ltac/pptactic.mli')
| -rw-r--r-- | plugins/ltac/pptactic.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 19bdf2d49..4265c416b 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -106,10 +106,6 @@ val pr_hintbases : string list option -> std_ppcmds val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds -val pr_bindings : - ('constr -> std_ppcmds) -> - ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds - val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> |