aboutsummaryrefslogtreecommitdiff
path: root/library/declaremods.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/declaremods.ml')
-rw-r--r--library/declaremods.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml
index b8dd671cfc..b58b355f7a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -436,7 +436,7 @@ let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 =
| [] -> () | _ -> anomaly "Unexpected functor objects" in
let rec replace_idl = function
| _,[] -> []
- | id::idl,(id',obj)::tail when id_eq id id' ->
+ | id::idl,(id',obj)::tail when Id.equal id id' ->
if not (String.equal (object_tag obj) "MODULE") then anomaly "MODULE expected!";
let substobjs = match idl with
| [] ->