diff options
| author | Pierre-Marie Pédrot | 2014-09-02 14:26:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-02 14:32:57 +0200 |
| commit | ac60d974cc028cef60eb3593d1778977c1636629 (patch) | |
| tree | 2dad4d45848cc94bf6db0997c124e91ba4145091 /printing | |
| parent | deebdaa96867dc4424d412956b3a2f595f4d4cc7 (diff) | |
Removing [revert] tactic from the AST.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f3bec78e20..f8eb93956e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -791,8 +791,6 @@ and pr_atom1 = function (fun (i1,i2) -> pr_ident i1 ++ spc () ++ str "into" ++ spc () ++ pr_ident i2) l) - | TacRevert l -> - hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l) (* Constructors *) | TacSplit (ev,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l) |