From 3c564fcc55efb3768e73ebc1e25b5e306fb925a1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Jan 2016 18:12:12 -0800 Subject: [PATCH] fix(library/user_recursors): 'print recursor-lemma' command --- src/library/user_recursors.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index d326693e6..ead18b112 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -354,7 +354,7 @@ void initialize_user_recursors() { is_user_defined_recursor, [](environment const & env, name const & d) { auto info = get_recursor_info(env, d); - return info.get_major_pos(); + return info.get_major_pos()+1; // internally major pos is 0-based }); }