diff options
| author | Maxime Dénès | 2017-06-12 16:20:15 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-12 16:43:33 +0200 |
| commit | 9097e9a84cf3841cd5fac81a7fe309ae2dec246f (patch) | |
| tree | 7358a5db6e5f6f17974cc61b4491248f30a332b4 /plugins/extraction/mlutil.ml | |
| parent | 013c0232953f1f5832c30940119da05847e99ce2 (diff) | |
| parent | b6feaafc7602917a8ef86fb8adc9651ff765e710 (diff) | |
Merge PR#718: API cleanup: aliases
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 5a50899c66..3a70a50204 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -29,9 +29,9 @@ let dummy_name = Id.of_string "_" let anonymous = Id anonymous_name let id_of_name = function - | Anonymous -> anonymous_name - | Name id when Id.equal id dummy_name -> anonymous_name - | Name id -> id + | Name.Anonymous -> anonymous_name + | Name.Name id when Id.equal id dummy_name -> anonymous_name + | Name.Name id -> id let id_of_mlid = function | Dummy -> dummy_name @@ -1488,7 +1488,7 @@ let inline_test r t = let con_of_string s = let d, id = Libnames.split_dirpath (dirpath_of_string s) in - Constant.make2 (MPfile d) (Label.of_id id) + Constant.make2 (ModPath.MPfile d) (Label.of_id id) let manual_inline_set = List.fold_right (fun x -> Cset_env.add (con_of_string x)) |