aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inductiveops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/inductiveops.ml')
-rw-r--r--pretyping/inductiveops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b0637a972..812900ea8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -79,7 +79,7 @@ let mis_is_recursive_subset listind rarg =
List.exists
(fun ra ->
match dest_recarg ra with
- | Mrec (_,i) -> List.mem i listind
+ | Mrec (_,i) -> Int.List.mem i listind
| _ -> false) rvec
in
Array.exists one_is_rec (dest_subterms rarg)