From 400327165edcba667ebb70ebb89052455656b719 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 19 Nov 2013 19:50:51 +0100 Subject: 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. --- library/declaremods.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/declaremods.ml') 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 -- cgit v1.2.3