aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind/indfun.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind/indfun.ml')
-rw-r--r--contrib/funind/indfun.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index d3e18371b..7385bf652 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -227,6 +227,8 @@ let rec is_rec names =
| RCases(_,_,el,brl) ->
List.exists (fun (e,_) -> lookup names e) el ||
List.exists (lookup_br names) brl
+ | RLetPattern (_,(c,_),p) ->
+ lookup names c || lookup_br names p
and lookup_br names (_,idl,_,rt) =
let new_names = List.fold_right Idset.remove idl names in
lookup new_names rt