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/libobject.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'library/libobject.mli') diff --git a/library/libobject.mli b/library/libobject.mli index e886c4db0..3986b3d3f 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -100,6 +100,7 @@ val declare_object : 'a object_declaration -> ('a -> obj) val object_tag : obj -> string +val object_has_tag : obj -> string -> bool val cache_object : object_name * obj -> unit val load_object : int -> object_name * obj -> unit -- cgit v1.2.3