From a0ea7ebf4838903c3ed9a9b885716cf14134a0c8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 1 Jun 2017 05:42:14 +0200 Subject: [printing] Remove duplicated printing function. It seems there were 4 copies of the same function in the code base. --- plugins/ltac/pptactic.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'plugins/ltac/pptactic.mli') 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) -> -- cgit v1.2.3