diff options
| author | letouzey | 2013-08-22 14:30:01 +0000 |
|---|---|---|
| committer | letouzey | 2013-08-22 14:30:01 +0000 |
| commit | f6d8fc17dc9474e4d043cf709d672d9259599354 (patch) | |
| tree | 3e05dce982c2bebb63f432064136d927a227e0c7 /plugins/extraction/mlutil.ml | |
| parent | 08e7ec2c48c5ca666ad42b5f969576e6aa43d2ea (diff) | |
Nicer code concerning dirpaths and modpath around Lib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 659ee4ec4b..0903f85a04 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1301,9 +1301,8 @@ let inline_test r t = not (is_fix t2) && ml_size t < 12 && is_not_strict t) let con_of_string s = - match DirPath.repr (dirpath_of_string s) with - | id :: d -> Constant.make2 (MPfile (DirPath.make d)) (Label.of_id id) - | [] -> assert false + let d, id = Libnames.split_dirpath (dirpath_of_string s) in + Constant.make2 (MPfile d) (Label.of_id id) let manual_inline_set = List.fold_right (fun x -> Cset_env.add (con_of_string x)) |