. — .
Reset local variable scope when checking with-clauses.
This fixes issue 562.
Internal change: Lazy monadic conjunction.
Added andM :: Monad m => [m Bool] -> m Bool to Agda.Utils.Monad. Typical uses: andM l (lazy) vs. and $ sequence l (strict) andM $ map f l (lazy) vs. and <$> mapM f l (strict)
A successful test for the combination of sized types and termination depth.
Fixed polarity computation. Must be done after positivity check.
Now, e.g., List is correctly recognized as covariant. This should fix some problems with sized types.
Workaround for the "Marker does not point anywhere" message.
Info buffer: Point is now (again) moved to the top when APPEND is nil.
fixed issue 552: new unifications weren't applied to the current substitution
Fixed bug: Highlighting was sometimes updated when it shouldn't.
Fixed bug: Highlighting info files were written when they shouldn't be.
Agda info buffer: Unmapped 'g', switched to compilation major mode.
Fixed bug: Killed Agda info buffers were not recreated automatically.
Debug messages are now printed in a buffer called *Agda debug*.
Function "absurd" generated for absurd lambda now applied to contextTelescope.
Changed the default for agda2-highlight-typechecks-face.
Fixed bug: Highlighting of errors was sometimes overwritten.
If text is appended to the info buffer, then point is placed at the end.
Fixed problem: Some commands were not echoed in the *ghci* buffer.
Fixed bug: Interactive highlighting aborted when ? turned into {!!}.
Emacs mode: Info about which module is currently being type-checked.