aboutsummaryrefslogtreecommitdiff
path: root/parsing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/printer.ml')
-rw-r--r--parsing/printer.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 3083154e60..c8059e37e5 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -77,6 +77,7 @@ let gentermpr_core at_top k env t =
with s -> wrap_exception s
let gentermpr k = gentermpr_core false k
+let gentermpr_at_top k = gentermpr_core true k
let prterm_env_at_top a = gentermpr_core true CCI a
let prterm_env a = gentermpr CCI a