aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/pptactic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/pptactic.ml')
-rw-r--r--plugins/ltac/pptactic.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 85bb901046..cbb53497d3 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -179,7 +179,7 @@ let string_of_genarg_arg (ArgumentType arg) =
| ConstrTypeOf c ->
hov 1 (keyword "type of" ++ spc() ++ prc env sigma c)
| ConstrTerm c when test c ->
- h 0 (str "(" ++ prc env sigma c ++ str ")")
+ h (str "(" ++ prc env sigma c ++ str ")")
| ConstrTerm c ->
prc env sigma c