 Jesper Cockx
|
848d9ef8dc
[ re #3116 ] Small fix in Changelog
|
6 years ago |
|
Jesper Cockx
|
275efccf44
[ prop ] Add user manual + changelog
|
6 years ago |
|
Jesper Cockx
|
cc7fa23633
[ generalize ] It's fine to shadow generalizable variables during printing
|
6 years ago |
|
Jesper Cockx
|
90c005d48d
[ fix #3433 ] Turn Prop into Set for checking sort of indices
|
6 years ago |
|
Jesper Cockx
|
002ff33df4
[ fix #3032 ] Use `printMetasBare` for interactive case splitting
|
6 years ago |
|
Jesper Cockx
|
b4b2b72e57
[ fix #3439 ] With --type-in-type, `Setω` is equal to any `Set l`
|
6 years ago |
 Andrés Sicard-Ramírez
|
1119fb0dec
[ closed #3442 ] Supported GHC 8.6.3.
|
6 years ago |
|
Jesper Cockx
|
c97a7abe0c
[ #3446 ] Added to Changelog
|
6 years ago |
|
Jesper Cockx
|
4f2ef57d87
[ #3095 ] Treat pattern variables bound in parent clause as module parameters
|
6 years ago |
|
Jesper Cockx
|
146b9aa03d
[ #3114 ] Test case
|
6 years ago |
|
Jesper Cockx
|
dabcd1c756
[ #572 ] Print qualified name for shadowed definitions
|
6 years ago |
|
Jesper Cockx
|
ad216a4cf1
[ #3445 ] Test case
|
6 years ago |
|
Jesper Cockx
|
20bf052087
[ re #572 ] Explicitly show renaming of shadowed variables
|
6 years ago |
|
Jesper Cockx
|
6ce4505e65
[ re #572 ] Properly deal with shadowed names (finally!)
|
6 years ago |
|
Jesper Cockx
|
c487b8a2be
[ abstractToConcrete ] Improved strategy for choosing names
|
6 years ago |
|
Jesper Cockx
|
e060f2d4eb
[ refactor ] Simplify call to CheckWithFunctionType
|
6 years ago |
|
Jesper Cockx
|
b42ac7eb50
[ refactor ] Use QName instead of Name for CheckDataDef/RecDef/FunDef/...
|
6 years ago |
|
Jesper Cockx
|
832dffbc8b
[ refactor ] Move logic for generating name variants from Abstract to Concrete
|
6 years ago |
|
Jesper Cockx
|
242c3be5e8
[ #3127 ] Remove prefix for out-of-scope names altogether
|
6 years ago |
|
Andrés Sicard-Ramírez
|
4c096a4093
[ #3128 ] Added CHANGELOG entry.
|
6 years ago |
|
Andrés Sicard-Ramírez
|
7e0fe82fad
[ fixed #3128 ] Fixed typo (Builtins -> Builtin).
|
6 years ago |
 Nils Anders Danielsson
|
18ffdbca01
[ agda-bisect ] A script exit code of 127 now means "skip".
|
6 years ago |
|
Nils Anders Danielsson
|
e861e24569
[ agda-bisect ] Scripts are now given absolute paths to Agda.
|
6 years ago |
|
Nils Anders Danielsson
|
26a5eae26f
[ agda-bisect ] Added --cache.
|
6 years ago |
 Ulf Norell
|
40978c66cf
[ fix #2579 ] changelog
|
6 years ago |
|
Ulf Norell
|
b4a4809804
[ fix #3436 ] generalizable variable in data/record type with missing definition
|
6 years ago |
|
Ulf Norell
|
424cf62360
[ fix #3169 ] point to rewrite documentation in rewriting stub
|
6 years ago |
|
Ulf Norell
|
cd5315aa0a
[ fix #3343 ] bad generator for QuickCheck test
|
6 years ago |
|
Ulf Norell
|
fa3967e214
[ fix #3195 ] internal error in auto
|
6 years ago |
|
Ulf Norell
|
6b1120845f
[ fix #2089 ] less rude error message
|
6 years ago |
