title: Can composing try and repeat lead to an infinite loop in Coq?
body: <p>I know that repeat applies a tactical multiple times until it fails. </p>
  
  <blockquote>
    <p>The repeat tactical takes another tactic and keeps applying this tactic until it fails.</p>
  </blockquote>
  
  <p>and the try tactic does nothing when it "fails":</p>
  
  <blockquote>
    <p>If T is a tactic, then try T is a tactic that is just like T except that, if T fails, try T successfully does nothing at all (instead of failing).</p>
  </blockquote>
  
  <p>does that mean if I were to do something like:</p>
  
  <pre><code>repeat (try reflexivity).
  </code></pre>
  
  <p>if the reflexivity fails then try does nothing (but not fail) so repeat just keeps applying <code>try reflexivity</code>. Is this correct? Or what is going?</p>
  
  <hr>
  
  <p>The reason I ask is because I saw this theorem:</p>
  
  <pre><code>Theorem In10 : In 10 [1;2;3;4;5;6;7;8;9;10].
  Proof.
    repeat (try (left; reflexivity); right).
  Qed.
  </code></pre>
  
  <p>when I asked a related question: <a href="https://stackoverflow.com/questions/53750496/are-coq-tacticals-right-associative-or-left-associative">Are Coq tacticals right associative or left associative?</a></p>
  
  <p>source: <a href="https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html" rel="nofollow noreferrer">https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html</a></p>