diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 633ff18762..114410fed1 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -900,17 +900,6 @@ module Make pr_opt pr_eliminator el ) - (* Context management *) - | TacRename l -> - hov 1 ( - primitive "rename" ++ brk (1,1) - ++ prlist_with_sep - (fun () -> str "," ++ brk (1,1)) - (fun (i1,i2) -> - pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2) - l - ) - (* Conversion *) | TacReduce (r,h) -> hov 1 ( |