From b2beb9087628de23679a831e6273b91816f1ed27 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 17 Dec 2015 19:24:17 +0100
Subject: Using dynamic values in tactic evaluation.

---
 dev/top_printers.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0e90026122..20c8f690bd 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -467,11 +467,13 @@ let pp_generic_argument arg =
   pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">")
 
 let prgenarginfo arg =
-  let tpe = pr_argument_type (genarg_tag arg) in
-  try
-    let data = Pptactic.pr_top_generic (Global.env ()) arg in
-    str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >"
-  with _any ->
+  let Val.Dyn (tag, _) = arg in
+  let tpe = str (Val.repr tag) in
+  (** FIXME *)
+(*   try *)
+(*     let data = Pptactic.pr_top_generic (Global.env ()) arg in *)
+(*     str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" *)
+(*   with _any -> *)
     str "<genarg:" ++ tpe ++ str ">"
 
 let ppgenarginfo arg = pp (prgenarginfo arg)
-- 
cgit v1.2.3