aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-04-08 00:58:56 +0200
committerPierre-Marie Pédrot2016-04-08 01:44:10 +0200
commitb5420538da04984ca42eb4284a9be27f3b5ba021 (patch)
treeaef40fc7c5b541e47a15e62488ca617b96012f78 /dev
parent1f6a31d138bcfcf341f28772de7c5e08906167c5 (diff)
Fixing printing of toplevel values.
This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all.
Diffstat (limited to 'dev')
-rw-r--r--dev/top_printers.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 141eab3f3f..29ea08e025 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -468,7 +468,7 @@ let pp_generic_argument arg =
let prgenarginfo arg =
let Val.Dyn (tag, _) = arg in
- let tpe = Val.repr tag in
+ let tpe = Val.pr tag in
(** FIXME *)
(* try *)
(* let data = Pptactic.pr_top_generic (Global.env ()) arg in *)