diff options
| author | Pierre Letouzey | 2015-12-15 17:46:25 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2015-12-15 18:07:47 +0100 |
| commit | 3c535011374382bc205a68b1cb59cfa7247d544a (patch) | |
| tree | ea4284d56483b42746720df97a33a86471d4888a /plugins/extraction/mlutil.ml | |
| parent | a110ddfd6fc040a805de3f0ec2995b51ff301f5c (diff) | |
Extraction: fix a few little glitches with my last commit (replacing unused vars by _)
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 2b606bf13c..eb3046f031 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -514,11 +514,6 @@ let nb_occur_match = (* Replace unused variables by _ *) let dump_unused_vars a = - let dump_id = function - | Dummy -> Dummy - | Id _ -> Id dummy_name - | Tmp _ -> Tmp dummy_name - in let rec ren env a = match a with | MLrel i -> let () = (List.nth env (i-1)) := true in a @@ -527,7 +522,7 @@ let dump_unused_vars a = let occ_id = ref false in let b' = ren (occ_id::env) b in if !occ_id then if b' == b then a else MLlam(id,b') - else MLlam(dump_id id,b') + else MLlam(Dummy,b') | MLletin (id,b,c) -> let occ_id = ref false in @@ -537,7 +532,7 @@ let dump_unused_vars a = if b' == b && c' == c then a else MLletin(id,b',c') else (* 'let' without occurrence: shouldn't happen after simpl *) - MLletin(dump_id id,b',c') + MLletin(Dummy,b',c') | MLcase (t,e,br) -> let e' = ren env e in @@ -572,7 +567,7 @@ let dump_unused_vars a = let b' = ren (List.rev_append occs env) b in let ids' = List.map2 - (fun id occ -> if !occ then id else dump_id id) + (fun id occ -> if !occ then id else Dummy) ids occs in if b' == b && List.equal eq_ml_ident ids ids' then tr |