diff options
Diffstat (limited to 'plugins')
| -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 |