aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/check_stat.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-04-28 13:58:25 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-04-28 13:58:25 +0200
commit5055ba0abd1a36d6f33666b0f72fbd9cf6ae3971 (patch)
treef5158b690ec3266d4126504777e65908aa22716e /checker/check_stat.ml
parente5fe4569f3eaeaa4e1ce377989e19f1f2c176da9 (diff)
Fix missing newline in coqchk engagement (bug #4694).
Diffstat (limited to 'checker/check_stat.ml')
-rw-r--r--checker/check_stat.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index d031975d7..84f5684d4 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -28,7 +28,7 @@ let pr_engagement (impr_set,type_in_type) =
match impr_set with
| ImpredicativeSet -> str "Theory: Set is impredicative"
| PredicativeSet -> str "Theory: Set is predicative"
- end ++
+ end ++ fnl() ++
begin
match type_in_type with
| StratifiedType -> str "Theory: Stratified type hierarchy"