diff options
| author | William Lawvere | 2017-06-13 22:22:36 -0700 |
|---|---|---|
| committer | William Lawvere | 2017-06-13 22:22:36 -0700 |
| commit | af39f62ad21f71a860e287e4d217b24dc9e2106b (patch) | |
| tree | 43c14ae184f24fffaf495dade6d27a1c2fac3e1a /plugins/extraction/mlutil.ml | |
| parent | 3b0830ce0233db5b612e0b5bb92e89fa644eb0e4 (diff) | |
| parent | 7e63c300a3aa1e3befb29bab9094e8b1939824bb (diff) | |
Merge remote-tracking branch 'upstream/trunk' into trunk
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)) |