From c32728e7bf0ba0449b60ea49df7f92fb6b70923d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 5 Nov 2014 00:56:29 +0100
Subject: Removing the legacy intro tactic code.

---
 printing/printer.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'printing/printer.ml')

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" *)
-- 
cgit v1.2.3