aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega/const_omega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/romega/const_omega.ml')
-rw-r--r--plugins/romega/const_omega.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index af833dacb..5416e936c 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -23,7 +23,7 @@ let string_of_global r =
| [] -> ""
| m::_ ->
let s = Names.Id.to_string m in
- if List.mem s meaningful_submodule then s^"." else ""
+ if Util.String.List.mem s meaningful_submodule then s^"." else ""
in
prefix^(Names.Id.to_string (Nametab.basename_of_global r))