The repeat tactic now honors failure levels in ltac.
Cleanup of comments in bootstrap/Monads.v
Doc: solve the bad interaction between Declare Implicit Tactic and refine.

An implicit tactic was declared and made refine fail (trying to solve the open goals of the refined term resulted in an error). There was no way to remove the implicit tactic (it isn't managed by an option so isn't removed by Reset Initial). I added the option under the name Clear Implicit Tactic.
Update comments.