From ee162ba3b28fccca0a2b3ea4b1e0811006840570 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 24 Feb 2016 10:07:57 +0100
Subject: Removing the MetaIdArg entry of tactic expressions.

This was historically used together with the <:tactic< ... >> quotation to insert
foreign code as $foo, but it actually only survived in the implementation of Tauto.
With the removal of the quotation feature, this is now totally obsolete.
---
 printing/pptactic.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index ed85b21478..12667d0f24 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1189,10 +1189,6 @@ module Make
           else str"(" ++ strm ++ str")"
 
         and pr_tacarg = function
-          | MetaIdArg (loc,true,s) ->
-            pr_with_comments loc (str "$" ++ str s)
-          | MetaIdArg (loc,false,s) ->
-            pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s)
           | Reference r ->
             pr.pr_reference r
           | ConstrMayEval c ->
-- 
cgit v1.2.3