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.

1 files changed, 4 insertions, 2 deletions

diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index e8383bda59..6f354b1ce5 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -263,10 +263,12 @@ let dfix_to_mlfix rv av i =
    order to preserve the global interface, later [depcheck_se] will get
    rid of them if possible *)
 
+let optim_ast t = dump_unused_vars (normalize t)
+
 let rec optim_se top to_appear s = function
   | [] -> []
   | (l,SEdecl (Dterm (r,a,t))) :: lse ->
-      let a = normalize (ast_glob_subst !s a) in
+      let a = optim_ast (ast_glob_subst !s a) in
       let i = inline r a in
       if i then s := Refmap'.add r a !s;
       let d = match optimize_fix a with
@@ -276,7 +278,7 @@ let rec optim_se top to_appear s = function
       in
       (l,SEdecl d) :: (optim_se top to_appear s lse)
   | (l,SEdecl (Dfix (rv,av,tv))) :: lse ->
-      let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in
+      let av = Array.map (fun a -> optim_ast (ast_glob_subst !s a)) av in
       (* This fake body ensures that no fixpoint will be auto-inlined. *)
       let fake_body = MLfix (0,[||],[||]) in
       for i = 0 to Array.length rv - 1 do