diff --git a/src/library/tactic/user_attribute.cpp b/src/library/tactic/user_attribute.cpp index 4e12b87762..d5e144f8bd 100644 --- a/src/library/tactic/user_attribute.cpp +++ b/src/library/tactic/user_attribute.cpp @@ -24,23 +24,6 @@ Author: Sebastian Ullrich namespace lean { -/* typed_attribute */ -struct user_attr_data : public attr_data { - // to be filled - - void write(serializer &) const { - lean_unreachable(); - } - void read(deserializer &) { - lean_unreachable(); - } -}; - -class user_attribute : public typed_attribute { -public: - user_attribute(name const & id, char const * descr) : typed_attribute(id, descr) {} -}; - /* Persisting */ struct user_attr_ext : public environment_extension { name_map m_attrs; @@ -74,7 +57,7 @@ static environment add_user_attr(environment const & env, name const & d) { std::string descr = to_string(cfield(o, 1)); user_attr_ext ext = get_extension(env); - ext.m_attrs.insert(n, attribute_ptr(new user_attribute(n, descr.c_str()))); + ext.m_attrs.insert(n, attribute_ptr(new basic_attribute(n, descr.c_str()))); return update(env, ext); } diff --git a/tests/lean/caching_user_attribute.lean b/tests/lean/caching_user_attribute.lean index 1dd97b5d2a..663d65f9df 100644 --- a/tests/lean/caching_user_attribute.lean +++ b/tests/lean/caching_user_attribute.lean @@ -10,21 +10,12 @@ set_option trace.user_attributes_cache true run_cmd do s : string ← caching_user_attribute.get_cache foo_attr, - tactic.trace s - -run_cmd do - s : string ← caching_user_attribute.get_cache foo_attr, - tactic.trace s - -attribute [foo] eq.mpr -local attribute [-foo] eq.mp - -run_cmd do - s : string ← caching_user_attribute.get_cache foo_attr, - tactic.trace s - -attribute [reducible] eq.mp -- should not affect [foo] cache - -run_cmd do + tactic.trace s, + s : string ← caching_user_attribute.get_cache foo_attr, + tactic.trace s, + tactic.set_basic_attribute `foo ``eq.mpr, + s : string ← caching_user_attribute.get_cache foo_attr, + tactic.trace s, + tactic.set_basic_attribute `reducible ``eq.mp, -- should not affect [foo] cache s : string ← caching_user_attribute.get_cache foo_attr, tactic.trace s diff --git a/tests/lean/caching_user_attribute.lean.expected.out b/tests/lean/caching_user_attribute.lean.expected.out index d51bcb46ed..e07241d131 100644 --- a/tests/lean/caching_user_attribute.lean.expected.out +++ b/tests/lean/caching_user_attribute.lean.expected.out @@ -3,16 +3,16 @@ eq.refl eq.mp -[user_attributes_cache] no cached result for [foo] -[user_attributes_cache] recomputing cache for [foo] eq.refl eq.mp -[user_attributes_cache] no cached result for [foo] +[user_attributes_cache] cached result for [foo] has been found, but cache fingerprint does not match [user_attributes_cache] recomputing cache for [foo] eq.refl +eq.mp eq.mpr eq.refl +eq.mp eq.mpr