diff options
| author | Matej Kosik | 2015-12-16 16:19:51 +0100 |
|---|---|---|
| committer | Matej Kosik | 2016-01-11 14:59:26 +0100 |
| commit | a1aff01d16bad2f44392fd5cb804092e12e558ed (patch) | |
| tree | bd2a1faf08b1c399171a308cf45bfd46d60ab5c5 /plugins/funind | |
| parent | 78bad016e389cd78635d40281bfefd7136733b7e (diff) | |
CLEANUP: removing unused field
I have removed the second field of the "Constrexpr.CRecord" variant
because once it was set to "None"
it never changed to anything else.
It was just carried and copied around.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 7815a8f818..d1e1098259 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -752,10 +752,8 @@ let rec add_args id new_args b = | CCast(loc,b1,b2) -> CCast(loc,add_args id new_args b1, Miscops.map_cast_type (add_args id new_args) b2) - | CRecord (loc, w, pars) -> - CRecord (loc, - (match w with Some w -> Some (add_args id new_args w) | _ -> None), - List.map (fun (e,o) -> e, add_args id new_args o) pars) + | CRecord (loc, pars) -> + CRecord (loc, List.map (fun (e,o) -> e, add_args id new_args o) pars) | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation") | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization") | CPrim _ -> b |