diff options
| author | Pierre-Marie Pédrot | 2016-05-09 00:12:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-03 16:51:09 +0200 |
| commit | 3206bf597d63066d9d9f8adfd0fe76e3c1c97e4d (patch) | |
| tree | 8134c12bef64decc00490519f2f04e06932355e0 /printing | |
| parent | 5cd0310f061b5eb1a631a0fff0ee7eb9674a11c3 (diff) | |
Removing "rename" from the tactic AST.
Diffstat (limited to 'printing')
| -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 ( |