aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/depends.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/depends.ml')
-rw-r--r--contrib/interface/depends.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index e7c6c5bcb..203bc9e3d 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -210,8 +210,6 @@ let rec depends_of_rawconstr rc acc = match rc with
| RLambda (_, _, _, rct, rcb)
| RProd (_, _, _, rct, rcb)
| RLetIn (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc)
- | RRecord (_, w, l) -> depends_of_rawconstr_list (List.map snd l)
- (Option.fold_right depends_of_rawconstr w acc)
| RCases (_, _, rco, tmt, cc) ->
(* LEM TODO: handle the cc *)
(Option.fold_right depends_of_rawconstr rco