diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-19 19:50:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-22 00:31:15 +0100 |
| commit | 400327165edcba667ebb70ebb89052455656b719 (patch) | |
| tree | bb75fbc10f2c43861e13de90df02e188e64078d3 /library/declaremods.ml | |
| parent | 433fe369bc95d7fe2086cf2256d85443b2420f34 (diff) | |
Using hashes instead of strings in dynamic tags. In case of collision, an
anomaly is raised. As there are very few tags defined in Coq code, this is
very unlikely to appear, and can be fixed by tweaking the name of the
dynamic argument.
This should be more efficient, as we did compare equal strings each time.
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index dae585d5a..c60e008d1 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -369,7 +369,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 (String.equal (object_tag obj) "MODULE"); + assert (object_has_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 |