diff options
Diffstat (limited to 'interp/modintern.ml')
| -rw-r--r-- | interp/modintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index 1e7d84c96c..ba5c68a5d9 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -77,7 +77,7 @@ let lookup_qualid (modtype:bool) qid = in let rec find_module_prefix dir n = if n<0 then raise Not_found; - let dir',dir'' = list_chop n dir in + let dir',dir'' = List.chop n dir in let id',dir''' = match dir'' with | hd::tl -> hd,tl |