From eee16239f6b00400c8a13b787c310bcb11c37afe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Dec 2015 12:06:24 +0100
Subject: Tying the loop in tactic printing API.

---
 dev/top_printers.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b3b1ae0e91..0e90026122 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -468,9 +468,8 @@ let pp_generic_argument arg =
 
 let prgenarginfo arg =
   let tpe = pr_argument_type (genarg_tag arg) in
-  let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in
   try
-    let data = Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg in
+    let data = Pptactic.pr_top_generic (Global.env ()) arg in
     str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >"
   with _any ->
     str "<genarg:" ++ tpe ++ str ">"
-- 
cgit v1.2.3