From af0f8bcd294f0ada958b0eff2bc2b335f212866e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Sep 2016 17:57:01 -0700 Subject: [PATCH] fix(library/explicit): annotation name --- src/library/explicit.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/library/explicit.cpp b/src/library/explicit.cpp index 9dcc67f3b3..c0112ae068 100644 --- a/src/library/explicit.cpp +++ b/src/library/explicit.cpp @@ -36,10 +36,10 @@ bool is_as_atomic(expr const & e) { return is_annotation(e, *g_as_atomic_name); expr const & get_as_atomic_arg(expr const & e) { lean_assert(is_as_atomic(e)); return get_annotation_arg(e); } void initialize_explicit() { - g_explicit_name = new name("@@"); - g_partial_explicit_name = new name("@"); - g_as_atomic_name = new name("as_atomic"); - g_as_is_name = new name("as_is"); + g_explicit_name = new name("@"); + g_partial_explicit_name = new name("@@"); + g_as_atomic_name = new name("as_atomic"); + g_as_is_name = new name("as_is"); register_annotation(*g_explicit_name); register_annotation(*g_partial_explicit_name);