diff options
Diffstat (limited to 'plugins/extraction/modutil.ml')
| -rw-r--r-- | plugins/extraction/modutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 1211bbf17..8659de03e 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -30,7 +30,7 @@ let se_iter do_decl do_spec = | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' | MTwith (mt,ML_With_type(idl,l,t))-> let mp_mt = msid_of_mt mt in - let l',idl' = list_sep_last idl in + let l',idl' = List.sep_last idl in let mp_w = List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' in |