fix(frontends/lean/info_manager): std::set insert is a noop if set already contains an equivalent element

src/frontends/lean/info_manager.cpp

@@ -350,7 +350,9 @@ struct info_manager::imp {
                 ++it;
             }
         }
-        m_env_info.insert(env_info(l, m_iteration, env, o));
+        env_info info(l, m_iteration, env, o);
+        m_env_info.erase(info);
+        m_env_info.insert(info);
     }
 
     static bool is_tactic_type(expr const & e) {

tests/lean/interactive/info.input

@@ -0,0 +1,14 @@
+VISIT info.lean
+SYNC 9
+import logic
+-- print "hello"
+theorem tst (a b : Prop) : a ∧ b → b ∧ a :=
+begin
+  intro H,
+  apply and.intro,
+  apply (and.elim_right H),
+  apply (and.elim_left H),
+end
+WAIT
+INFO 6
+INFO 7

tests/lean/interactive/info.input.expected.out

@@ -0,0 +1,27 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- TYPE|6|8
+?M_1 → ?M_2 → ?M_1 ∧ ?M_2
+-- ACK
+-- IDENTIFIER|6|8
+and.intro
+-- ACK
+-- ENDINFO
+-- BEGININFO
+-- SYMBOL|7|8
+(
+-- ACK
+-- TYPE|7|9
+a ∧ b → b
+-- ACK
+-- IDENTIFIER|7|9
+and.elim_right
+-- ACK
+-- TYPE|7|24
+a ∧ b
+-- ACK
+-- IDENTIFIER|7|24
+H
+-- ACK
+-- ENDINFO