aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declaremods.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-05 12:53:20 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-05 13:38:14 +0100
commit895d34a264d9d90adfe4f0618c3bb0663dc01615 (patch)
treeda8406b2fd882318c8264487596f2aca0e5f9f2a /library/declaremods.ml
parent8596423ed6345495ca5ec0aedb8a9a431bee2e5d (diff)
Leveraging GADTs to provide a better Dyn API.
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 7f607a51c..d8c5ab5e7 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -371,7 +371,7 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 =
match idl, objs0 with
| _,[] -> []
| id::idl,(id',obj)::tail when Id.equal id id' ->
- assert (object_has_tag obj "MODULE");
+ assert (String.equal (object_tag obj) "MODULE");
let mp_id = MPdot(mp0, Label.of_id id) in
let objs = match idl with
| [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1