diff options
Diffstat (limited to 'checker/closure.ml')
| -rw-r--r-- | checker/closure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index c2708e97d..cef1d31a6 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -29,7 +29,7 @@ let reset () = beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0 let stop() = - msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ + Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]") |