HIGH PRIORITY:
  - We need a way of naming mutants so that, for example, we can test just a
    single mutant (that we have just added) instead of all mutants.  I'm
    going to guess that this will be so common a usage mode that we are
    going to want to name ALL mutants.  This will also be a more convenient
    way of printing them than printing diffs.
  - We probably also need a syntax for nested mutants

  - When displaying counterexamples, would it be easy to print the name of
    each bound variable along with the failing value that's been found for
    it? 

  - The top-level QC interface should expose as little as possible, so that
    modules that Import QC do not have their namespaces too polluted.  (And
    there should be a single file that most users import, rather than
    several.)
        - At the moment, most files that use QC include this at the top -- how
          much of it is really needed??
                 From QuickChick Require Export QuickChick.
                 Set Bullet Behavior "Strict Subproofs".
                 Import QcNotation. Open Scope qc_scope.
                 Import GenLow GenHigh.
                 Require Import List ZArith.
                 Import ListNotations.
                 Set Warnings "-extraction-opaque-accessed,-extraction".
                 Unset Refine Instance Mode.  (* Don't be too automatic! *)

  - Can we try again to fix the "Section... extends..." parsing issue?

  * Make a simpler tactic for deriving equality.
       Derive Arbitrary, Show, Eq for file_access_mode.
  * play with precedence for ? -- should bind tigher than implication
       - and could we automatically make decidable props checkable, without ?

MINOR:
  - Figure out how to check different mutants in parallel 
  - Catch C-c and terminate QC tool 
  - Add
       Set Warnings "-notation-overridden,-parsing".
    to all .v files to get rid of compilation warnings.
  - eliminate the rest of the compilation warnings (including nonexhaustive
    patterns!) 

COSMETIC:
  - Document (for emacs compile users):
      (require 'ansi-color)
      (defun endless/colorize-compilation ()
        "Colorize from `compilation-filter-start' to `point'."
        (let ((inhibit-read-only t))
          (ansi-color-apply-on-region
           compilation-filter-start (point))))

      (add-hook 'compilation-filter-hook
                #'endless/colorize-compilation)  

ABOUT DECIDABILITY:
  - Can we make every EqDec automatically be a Dec?
  - Dec seems not to be working as intended.  Leo hoped that the ? would not
    be necessary to coerce a (decidable) Prop to a Checkable...
  - How do I create a Dec instance for options?  
  - How should we phrase specs like the one for filesystem operations in DW?
    Is there a way of using Dec to (semi?-)automatically calculate decision
    procedures for things like /\ and forall formulas?

TASKS FOR THE SUMMER SCHOOL:
  - documentation -- coqdoc comments, especially on the most user-visible
    parts!
  - update and test opam package