aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/mod_checking.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-26 15:04:02 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-26 16:00:31 +0100
commit2919e4a927a4574a28012ae4ba9523e01fed1360 (patch)
tree41dec3a4166b257c4deed07c08ce4fb361684e4c /checker/mod_checking.ml
parent3bcd71163e5645aa6a0becedfbb2768389469d25 (diff)
coqchk: flush the pp buffer from time to time
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r--checker/mod_checking.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 521d9e3ee..9e61d3491 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -24,7 +24,7 @@ let refresh_arity ar =
| _ -> ar, Univ.empty_constraint
let check_constant_declaration env kn cb =
- Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn);
+ Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); pp_flush ();
let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in
let envty, ty =
match cb.const_type with