From 0b812bc91d1f5d4736fbd610e88fa7bf25f50960 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 28 Apr 2016 15:59:09 -0700 Subject: [PATCH] fix(kernel/declaration): typo and restoring trusted flag for constants --- src/kernel/declaration.h | 2 +- src/library/kernel_serializer.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 71fd4db297..d86c46b912 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -77,7 +77,7 @@ declaration mk_definition(environment const & env, name const & n, level_param_n declaration mk_theorem(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v); declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, unsigned w); declaration mk_axiom(name const & n, level_param_names const & params, expr const & t); -declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted = false); +declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted = true); void initialize_declaration(); void finalize_declaration(); diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index 63d43d587c..f160a5cb04 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -326,7 +326,7 @@ declaration read_declaration(deserializer & d) { if (is_th_ax) return mk_axiom(n, ps, t); else - return mk_constant_assumption(n, ps, t); + return mk_constant_assumption(n, ps, t, is_trusted); } }