diff options
| author | Maxime Dénès | 2017-06-05 22:32:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-05 22:32:11 +0200 |
| commit | 5a5d37b83c487903963aa39799a1367752857da4 (patch) | |
| tree | ca0ef708964eae74cbc24fc30c570fcea22f991d /plugins/ltac/pptactic.mli | |
| parent | 9a618ee0529f7153da1e10a8099a0b691bd13251 (diff) | |
| parent | a0ea7ebf4838903c3ed9a9b885716cf14134a0c8 (diff) | |
Merge PR#722: [printing] Remove duplicated printing function.
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 19bdf2d49f..4265c416b6 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) -> |