From 0aba678e885fa53fa649de59eb1d06b4af3a847c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Dec 2015 20:42:07 +0100
Subject: Getting rid of the dynamic node of the tactic AST.

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

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 766222156a..97917d2c72 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1263,9 +1263,6 @@ module Make
           else str"(" ++ strm ++ str")"
 
         and pr_tacarg = function
-          | TacDynamic (loc,t) ->
-            pr_with_comments loc
-              (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>")
           | MetaIdArg (loc,true,s) ->
             pr_with_comments loc (str "$" ++ str s)
           | MetaIdArg (loc,false,s) ->
-- 
cgit v1.2.3