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/libobject.mli | |
| 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/libobject.mli')
| -rw-r--r-- | library/libobject.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |