From 2c01bd7b446c1151922ad0a01c3dc6b85f5bea54 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 Apr 2016 19:27:30 +0200
Subject: Removing "double induction" from the tactic AST.

---
 printing/pptactic.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 44c832bd7a..5192e2db12 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -909,12 +909,6 @@ module Make
                 pr_opt (pr_clauses None pr.pr_name) cl) l ++
               pr_opt pr_eliminator el
           )
-        | TacDoubleInduction (h1,h2) ->
-          hov 1 (
-            primitive "double induction"
-            ++ pr_arg pr_quantified_hypothesis h1
-            ++ pr_arg pr_quantified_hypothesis h2
-          )
 
         (* Context management *)
         | TacRename l ->
-- 
cgit v1.2.3