aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppconstr.ml')
-rw-r--r--parsing/ppconstr.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 4970ca131..934850072 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -223,14 +223,14 @@ let surround_binder k p =
match k with
| Default b -> hov 1 (surround_impl b p)
| Generalized (b, b', t) ->
- hov 1 (surround_impl b' (surround_impl b p))
+ hov 1 (str"`" ++ (surround_impl b' p))
let surround_implicit k p =
match k with
| Default Explicit -> p
| Default Implicit -> (str"{" ++ p ++ str"}")
| Generalized (b, b', t) ->
- surround_impl b' (surround_impl b p)
+ str"`" ++ (surround_impl b' p)
let pr_binder many pr (nal,k,t) =
match t with