diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index c61b80c834..b1d6fb0c0f 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -898,11 +898,6 @@ module Make ) (* Context management *) - | TacClearBody l -> - hov 1 ( - primitive "clearbody" ++ spc () - ++ prlist_with_sep spc pr.pr_name l - ) | TacMove (id1,id2) -> hov 1 ( primitive "move" |