diff options
Diffstat (limited to 'checker/check_stat.mli')
| -rw-r--r-- | checker/check_stat.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/checker/check_stat.mli b/checker/check_stat.mli index 0cda7f0c8a..b094da1c44 100644 --- a/checker/check_stat.mli +++ b/checker/check_stat.mli @@ -7,9 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Safe_typing - val memory_stat : bool ref val output_context : bool ref -val stats : safe_environment -> unit +val stats : Environ.env -> unit |