diff options
| author | Pierre-Marie Pédrot | 2014-11-05 00:56:29 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-11-07 18:41:22 +0100 |
| commit | c32728e7bf0ba0449b60ea49df7f92fb6b70923d (patch) | |
| tree | aa4221a0343c0095808010f15fb5dbb1a4efe237 /printing/printer.ml | |
| parent | b320666d84e2f9b91d0ab6dd70f29cdb7da68818 (diff) | |
Removing the legacy intro tactic code.
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 5b88e8c98f..af81e192d1 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -652,9 +652,6 @@ let pr_goal_by_id id = (* Elementary tactics *) let pr_prim_rule = function - | Intro id -> - str"intro " ++ pr_id id - | Cut (b,replace,id,t) -> if b then (* TODO: express "replace" *) |