aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/detyping.ml')
-rw-r--r--pretyping/detyping.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 545366a70..2db867fc5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -85,7 +85,7 @@ module PrintingCasesIf =
PrintingInductiveMake (struct
let encode = encode_bool
let field = "If"
- let title = "Types leading to pretty-printing of Cases using a `if' form: "
+ let title = "Types leading to pretty-printing of Cases using a `if' form:"
let member_message s b =
str "Cases on elements of " ++ s ++
str