diff options
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" *) |