anchor.diff:            <h2>The effects system</h2>
             <p>What is the definition of a computation with IO and how does this work?</p>
   
  -          <h3>Effect</h3>
  +          <h3>Effects</h3>
             <p>An effect describes a set of IO or impure operations. An effect is declared by an element of type <code>Effect.t</code>:</p>
             <pre>Module Effect.
     Record t := New {
  
positive.code:             <li>the run of <code>C.Choose e1 e2</code> is either a run of <code>e1</code> or a run of <code>e2</code>;</li>
              <li>the run of <code>C.Join e1 e2</code> is the run of <code>e1</code> and a run of <code>e2</code>. Even if these two runs may actually interact, we are only interested in their projections on <code>e1</code> and <code>e2</code>.</li>
            </ul>
          </div>
        </div>
  <%= footer %>
  
negative.code:           </ul>
            <p>This use case is parametrized by a string <em>name</em>. We could write a test program interacting with <code>your_name</code>, answering the <em>name</em> string to the <code>read_line</code> request and checking that the program outputs are as expected. The limitation of this method is that we can only test a finite number of <em>name</em> values, instead of all the possible strings.</p>
  
            <h3>Runs</h3>
            <p>To cover all the use case instances, Coq.io introduces the notion of <em>run</em>. A run describes one execution of a computation, by programming the behavior of the computation's environment in a particular execution. Said otherwise, a run contains two programs: the computation itself and its environment, with typing rules ensuring that the environment answers to each request of the computation.</p>
            <p>A run is of type <code>Run.t e v</code>, where <code>e</code> is a computation and <code>v</code> is the expected result of the computation. We formally define this type by:</p>
            <pre>Module Run.
  