diff options
| author | herbelin | 2013-01-27 14:36:36 +0000 |
|---|---|---|
| committer | herbelin | 2013-01-27 14:36:36 +0000 |
| commit | 68b1fa3bceffef3c3dfef8b2f041f2e5eb4d3173 (patch) | |
| tree | affda6fb63631bc55245a1f08bc4af41cbbdb3de /pretyping | |
| parent | caff708cff41f6bb91d26b59f3d93018f17f63ba (diff) | |
Improving formatting of output of "Test table".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16159 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 545366a70f..2db867fc5c 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 |