diff options
| author | Pierre Letouzey | 2015-12-15 11:15:00 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2015-12-15 11:24:21 +0100 |
| commit | 4b197ed247d1f30ff40fa59f85b070766f305bea (patch) | |
| tree | 86f9a765c493bc1eaf2c3cabfbec64ad3cfa78d5 /plugins/extraction/mlutil.mli | |
| parent | ce395ca02311bbe6ecc1b2782e74312272dd15ec (diff) | |
Extraction: replace unused variable names by _ in funs and matchs (fix #2842)
This is done via a unique pass which seems roughly linear in practice,
even on big developments like CompCert. There's a List.nth in an env at
each MLrel, that could be made logarithmic if necessary via Okasaki's
skew list for instance.
Another approach would be to keep names (as a form of documentation), but
prefix them by _ to please OCaml's warnings. For now, let's be radical and
use the _ pattern.
Diffstat (limited to 'plugins/extraction/mlutil.mli')
| -rw-r--r-- | plugins/extraction/mlutil.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index c380dfb3e3..c07cee7136 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -111,6 +111,8 @@ val ast_subst : ml_ast -> ml_ast -> ml_ast val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast +val dump_unused_vars : ml_ast -> ml_ast + val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast val inline : global_reference -> ml_ast -> bool |