Refactor: lenses for Options to modify the TCState.
Cosmetics: renamed some identifiers and added a comment.
Fixed a broken failed test case (wrong filename instead of intended error).
Added default include dir $HOME/.cabal/share/Agda-x.y.z/lib/prim.
The path is communicated to Agda by cabal's generated Paths_Agda module.
Contains an empty module Agda.Prim so far.
Failed test suite machinery deletes the user- and version- specific parts of 
this path.
Added more author spellings.
HCAR November 2013.
Removed superfluous option --universe-polymorphism from two tests.
Fixed issue 930.  
Each of the two things fixes this issue:
* When sort comparison fails but type comparison succeeds, 
  try sort comparison again instead of throwing the old
  sort error.
* Fix sort comparison: pointwise comparison of Max not allowed
  if any term contains a meta (could be buried in a neutral level).
[release-notes] documented C-c C-h
removed unnecessary check from CheckInternal
Fixed a misspelling in Olle Fredriksson's name.
Issue 590: Reverted to the old behaviour.
Cosmetics: removed commented out code concerning elimView, added comments.
ElimView now only reduces projection-like functions.
This makes checkInternal more faithful, it reduces now
really only projection-like functions, which it needs
for bidirectional type-checking.
Pointless refactoring in DisplayForm.hs.
Cosmetics: separated constructor tools from datatype tools.
Clarified noShadowingOfConstructors code.  No need to normalize type!
Q: Should that not be checked for record constructors as well?
forMaybe is just flip mapMaybe.
More tests that pattern variables do not shadow constructors, for copatterns and flexible arity.
Now Agda.Prim contains the level primitives and is automatically imported.
Removed tons duplicate level builtin declarations from the test suite.
A problem remains in interaction/Error-in-imported-module:
An invalid emacs command is created there (with unterminated string).
  (agda2-highlight-load-and-delete-action "
I suspect that is because an __IMPOSSIBLE__, indicating a violated invariant,
is swallowed by a too general exception handler (Control.Exception.bracket)
in Agda.Interaction.Highlighting.Emacs.lispifyHighlightingInfo.
Probably an invariant concerning stModuleToSource is broken by my attempt
to fit the auto-import of Agda.Prim in a suitable place in 
Agda.Interaction.Imports.