aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-09-07 16:28:55 +0200
committerPierre-Marie Pédrot2017-09-07 16:28:55 +0200
commit643832c053e0255dd356231f4e5887db0228c2cd (patch)
treebbf14c2df595dc7ea8b82798cb9930618e327ff2 /src
parentd577fe086794fda2edb3b98c12606e24c9c92ea1 (diff)
Slightly better printing for anonymous closures.
Diffstat (limited to 'src')
-rw-r--r--src/tac2entries.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index d596a61152..7cffdc6590 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -757,7 +757,7 @@ let _ = Goptions.declare_bool_option {
}
let pr_frame = function
-| FrAnon e -> str "Call <anonymous:" ++ pr_glbexpr e ++ str ">"
+| FrAnon e -> str "Call {" ++ pr_glbexpr e ++ str "}"
| FrLtac kn ->
str "Call " ++ Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstant kn))
| FrPrim ml ->