diff options
| author | Pierre-Marie Pédrot | 2016-02-29 11:20:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-29 13:24:45 +0100 |
| commit | 7dd8c2bf4747c94be6f18d7fdd0e3b593f560a2f (patch) | |
| tree | 31301a44d27401d5fad006c9b400c9dd8f0d4d16 /printing | |
| parent | d0bc16d1a0626f4137797bbf0c91e972a0ff43ac (diff) | |
Moving the "clearbody" tactic to TACTIC EXTEND.
Diffstat (limited to 'printing')
| -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" |