From 146eaf5281a7771c7d7f8a1c2a44858ffdb27ad3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Jan 2017 11:49:05 -0800 Subject: [PATCH] fix(library/tactic/tactic_state): has_to_format universe changed see #1341 --- src/library/tactic/tactic_state.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 50b5450feb..931da56ab9 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -753,12 +753,12 @@ vm_obj tactic_decl_name(vm_obj const & _s) { format tactic_state::pp() const { type_context ctx = mk_type_context_for(*this, transparency_mode::Semireducible); expr ts_expr = mk_constant("tactic_state"); - optional to_fmt_inst = ctx.mk_class_instance(mk_app(mk_constant("has_to_format", {mk_level_one()}), ts_expr)); + optional to_fmt_inst = ctx.mk_class_instance(mk_app(mk_constant("has_to_format", {mk_level_zero()}), ts_expr)); if (!to_fmt_inst) { return pp_core(); } else { try { - expr code = mk_app(mk_constant("to_fmt", {mk_level_one()}), ts_expr, *to_fmt_inst); + expr code = mk_app(mk_constant("to_fmt", {mk_level_zero()}), ts_expr, *to_fmt_inst); expr type = ctx.infer(code); environment new_env = ctx.env(); bool use_conv_opt = true;