[agda] branch master updated (a654a1e -> 502b96c)
Iain Lane
laney at moszumanska.debian.org
Mon Jan 4 13:02:28 UTC 2016
This is an automated email from the git hooks/post-receive script.
laney pushed a change to branch master
in repository agda.
from a654a1e Finalise changelog & close bug
new 2fafd4d Imported Upstream version 2.4.2.3
new a116bca Imported Upstream version 2.4.2.5
new 457a205 Merge tag 'upstream/2.4.2.5'
new 2c258f5 Update build-deps for new release
new 7d835fa Remove patches which are applied upstream
new b5bd85b Update changelog
new 5fc7f86 Update mtl dep version
new 502b96c Finalise changelog
The 8 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails. The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.
Summary of changes:
Agda.cabal | 257 +-
CHANGELOG | 577 ++
LICENSE | 34 +-
README.md | 45 +-
debian/changelog | 8 +
debian/control | 37 +-
.../0001-.cabal-Supporting-only-cpphs-1.19.patch | 22 -
debian/patches/hashtables-dep | 37 -
debian/patches/series | 2 -
dist/build/Agda/Syntax/Parser/Lexer.hs | 475 --
dist/build/Agda/Syntax/Parser/Parser.hs | 5822 --------------------
src/agda-mode/Main.hs | 31 +-
src/data/EpicInclude/AgdaPrelude.e | 207 -
src/data/EpicInclude/stdagda.c | 95 -
src/data/EpicInclude/stdagda.h | 41 -
src/data/agda.sty | 1 +
src/data/emacs-mode/agda-input.el | 3 +-
src/data/emacs-mode/agda2-mode.el | 202 +-
src/data/emacs-mode/agda2.el | 6 +-
src/data/emacs-mode/annotation.el | 57 +-
src/full/Agda/Auto/Auto.hs | 645 ++-
src/full/Agda/Auto/CaseSplit.hs | 4 +-
src/full/Agda/Auto/Convert.hs | 11 +-
src/full/Agda/Auto/NarrowingSearch.hs | 17 +-
src/full/Agda/Auto/SearchControl.hs | 43 +-
src/full/Agda/Auto/Syntax.hs | 2 +-
src/full/Agda/Auto/Typecheck.hs | 6 +-
src/full/Agda/Benchmarking.hs | 109 +
src/full/Agda/Compiler/CallCompiler.hs | 2 +-
src/full/Agda/Compiler/Epic/CompileState.hs | 6 +-
src/full/Agda/Compiler/Epic/Compiler.hs | 5 +-
src/full/Agda/Compiler/Epic/Erasure.hs | 25 +-
src/full/Agda/Compiler/Epic/ForceConstrs.hs | 18 +-
src/full/Agda/Compiler/Epic/Forcing.hs | 8 +-
src/full/Agda/Compiler/Epic/FromAgda.hs | 10 +-
src/full/Agda/Compiler/Epic/Injection.hs | 23 +-
src/full/Agda/Compiler/Epic/Interface.hs | 2 +-
src/full/Agda/Compiler/Epic/NatDetection.hs | 4 +-
src/full/Agda/Compiler/Epic/Smashing.hs | 8 +-
src/full/Agda/Compiler/Epic/Static.hs | 12 +-
src/full/Agda/Compiler/HaskellTypes.hs | 2 +-
src/full/Agda/Compiler/JS/Compiler.hs | 17 +-
src/full/Agda/Compiler/MAlonzo/Compiler.hs | 521 +-
src/full/Agda/Compiler/MAlonzo/Compiler.hs-boot | 4 +-
src/full/Agda/Compiler/MAlonzo/Misc.hs | 19 +-
src/full/Agda/Compiler/MAlonzo/Primitives.hs | 8 +-
src/full/Agda/Interaction/BasicOps.hs | 162 +-
.../Interaction/{CommandLine => }/CommandLine.hs | 34 +-
src/full/Agda/Interaction/EmacsCommand.hs | 3 +-
src/full/Agda/Interaction/Exceptions.hs | 6 +-
src/full/Agda/Interaction/FindFile.hs | 14 +-
src/full/Agda/Interaction/Highlighting/Generate.hs | 99 +-
src/full/Agda/Interaction/Highlighting/HTML.hs | 61 +-
src/full/Agda/Interaction/Highlighting/LaTeX.hs | 4 +-
src/full/Agda/Interaction/Highlighting/Precise.hs | 18 +-
src/full/Agda/Interaction/Imports.hs | 252 +-
src/full/Agda/Interaction/InteractionTop.hs | 238 +-
src/full/Agda/Interaction/InteractionTop.hs-boot | 5 +
src/full/Agda/Interaction/MakeCase.hs | 169 +-
src/full/Agda/Interaction/Monad.hs | 21 +-
src/full/Agda/Interaction/Options.hs | 156 +-
src/full/Agda/Interaction/Response.hs | 7 +-
src/full/Agda/Interaction/Response.hs-boot | 12 -
src/full/Agda/Main.hs | 61 +-
src/full/Agda/Syntax/Abstract.hs | 102 +-
src/full/Agda/Syntax/Abstract/Copatterns.hs | 58 +-
src/full/Agda/Syntax/Abstract/Name.hs | 111 +-
src/full/Agda/Syntax/Abstract/Views.hs | 80 +-
src/full/Agda/Syntax/Common.hs | 228 +-
src/full/Agda/Syntax/Concrete.hs | 176 +-
src/full/Agda/Syntax/Concrete/Definitions.hs | 320 +-
src/full/Agda/Syntax/Concrete/Generic.hs | 9 +-
src/full/Agda/Syntax/Concrete/Name.hs | 67 +-
src/full/Agda/Syntax/Concrete/Operators.hs | 257 +-
src/full/Agda/Syntax/Concrete/Operators/Parser.hs | 69 +-
src/full/Agda/Syntax/Concrete/Pretty.hs | 117 +-
src/full/Agda/Syntax/Fixity.hs | 122 +-
src/full/Agda/Syntax/Fixity.hs-boot | 10 +
src/full/Agda/Syntax/Info.hs | 48 +-
src/full/Agda/Syntax/Internal.hs | 547 +-
src/full/Agda/Syntax/Internal/Defs.hs | 8 +-
src/full/Agda/Syntax/Internal/Generic.hs | 11 +-
src/full/Agda/Syntax/Internal/Pattern.hs | 38 +-
src/full/Agda/Syntax/Literal.hs | 2 +-
src/full/Agda/Syntax/Notation.hs | 11 +-
src/full/Agda/Syntax/Parser.hs | 7 +
src/full/Agda/Syntax/Parser/LookAhead.hs | 2 +-
src/full/Agda/Syntax/Parser/Monad.hs | 85 +-
src/full/Agda/Syntax/Parser/Parser.y | 564 +-
src/full/Agda/Syntax/Position.hs | 153 +-
src/full/Agda/Syntax/Scope/Base.hs | 118 +-
src/full/Agda/Syntax/Scope/Monad.hs | 160 +-
.../Agda/Syntax/Translation/AbstractToConcrete.hs | 315 +-
.../Agda/Syntax/Translation/ConcreteToAbstract.hs | 475 +-
.../Agda/Syntax/Translation/InternalToAbstract.hs | 549 +-
src/full/Agda/Termination/CallGraph.hs | 52 +-
src/full/Agda/Termination/CallMatrix.hs | 40 +-
src/full/Agda/Termination/CutOff.hs | 4 +-
src/full/Agda/Termination/Inlining.hs | 70 +-
src/full/Agda/Termination/Monad.hs | 201 +-
src/full/Agda/Termination/Order.hs | 28 +-
src/full/Agda/Termination/Semiring.hs | 16 -
src/full/Agda/Termination/SparseMatrix.hs | 42 +-
src/full/Agda/Termination/TermCheck.hs | 524 +-
src/full/Agda/Tests.hs | 14 +-
src/full/Agda/TypeChecking/Abstract.hs | 16 +-
src/full/Agda/TypeChecking/CheckInternal.hs | 62 +-
src/full/Agda/TypeChecking/CheckInternal.hs-boot | 1 +
src/full/Agda/TypeChecking/CompiledClause.hs | 73 +-
.../Agda/TypeChecking/CompiledClause/Compile.hs | 143 +-
src/full/Agda/TypeChecking/CompiledClause/Match.hs | 226 +-
src/full/Agda/TypeChecking/Constraints.hs | 9 +-
src/full/Agda/TypeChecking/Constraints.hs-boot | 1 +
src/full/Agda/TypeChecking/Conversion.hs | 709 ++-
src/full/Agda/TypeChecking/Coverage.hs | 110 +-
src/full/Agda/TypeChecking/Coverage/Match.hs | 6 +-
src/full/Agda/TypeChecking/DisplayForm.hs | 45 +-
src/full/Agda/TypeChecking/DropArgs.hs | 5 +-
src/full/Agda/TypeChecking/Empty.hs | 38 +-
src/full/Agda/TypeChecking/Errors.hs | 1835 +++---
src/full/Agda/TypeChecking/EtaContract.hs | 10 +-
src/full/Agda/TypeChecking/Forcing.hs | 162 +-
src/full/Agda/TypeChecking/Free.hs | 199 +-
src/full/Agda/TypeChecking/Free/Lazy.hs | 390 ++
.../Agda/TypeChecking/{Free.hs => Free/Old.hs} | 16 +-
src/full/Agda/TypeChecking/Free/Tests.hs | 125 +
src/full/Agda/TypeChecking/Implicit.hs | 22 +-
src/full/Agda/TypeChecking/Injectivity.hs | 8 +-
src/full/Agda/TypeChecking/InstanceArguments.hs | 239 +-
src/full/Agda/TypeChecking/Irrelevance.hs | 65 +-
src/full/Agda/TypeChecking/Level.hs | 6 +-
src/full/Agda/TypeChecking/MetaVars.hs | 599 +-
src/full/Agda/TypeChecking/MetaVars/Mention.hs | 9 +-
src/full/Agda/TypeChecking/MetaVars/Occurs.hs | 463 +-
src/full/Agda/TypeChecking/Monad.hs | 2 -
src/full/Agda/TypeChecking/Monad/Base.hs | 567 +-
src/full/Agda/TypeChecking/Monad/Base.hs-boot | 15 +-
src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs | 78 -
src/full/Agda/TypeChecking/Monad/Base/KillRange.hs | 120 -
src/full/Agda/TypeChecking/Monad/Benchmark.hs | 116 +-
src/full/Agda/TypeChecking/Monad/Builtin.hs | 86 +-
src/full/Agda/TypeChecking/Monad/Constraints.hs | 4 +-
src/full/Agda/TypeChecking/Monad/Context.hs | 29 +-
src/full/Agda/TypeChecking/Monad/Debug.hs | 6 -
src/full/Agda/TypeChecking/Monad/Exception.hs | 6 +-
src/full/Agda/TypeChecking/Monad/MetaVars.hs | 57 +-
src/full/Agda/TypeChecking/Monad/Mutual.hs | 9 +-
src/full/Agda/TypeChecking/Monad/Options.hs | 32 +-
src/full/Agda/TypeChecking/Monad/Signature.hs | 393 +-
src/full/Agda/TypeChecking/Monad/SizedTypes.hs | 17 +-
src/full/Agda/TypeChecking/Monad/State.hs | 25 +-
src/full/Agda/TypeChecking/Monad/Statistics.hs | 16 +-
src/full/Agda/TypeChecking/Monad/Trace.hs | 121 +-
src/full/Agda/TypeChecking/Patterns/Abstract.hs | 14 +-
src/full/Agda/TypeChecking/Patterns/Match.hs | 176 +-
src/full/Agda/TypeChecking/Patterns/Match.hs-boot | 2 +-
src/full/Agda/TypeChecking/Polarity.hs | 166 +-
src/full/Agda/TypeChecking/Positivity.hs | 454 +-
.../Agda/TypeChecking/Positivity/Occurrence.hs | 148 +
src/full/Agda/TypeChecking/Positivity/Tests.hs | 27 +
src/full/Agda/TypeChecking/Pretty.hs | 260 +-
src/full/Agda/TypeChecking/Pretty.hs-boot | 21 +-
src/full/Agda/TypeChecking/Primitive.hs | 335 +-
src/full/Agda/TypeChecking/ProjectionLike.hs | 141 +-
src/full/Agda/TypeChecking/Quote.hs | 12 +-
src/full/Agda/TypeChecking/RecordPatterns.hs | 145 +-
src/full/Agda/TypeChecking/Records.hs | 168 +-
src/full/Agda/TypeChecking/Reduce.hs | 185 +-
src/full/Agda/TypeChecking/Reduce/Monad.hs | 26 +-
src/full/Agda/TypeChecking/Rewriting.hs | 301 +-
src/full/Agda/TypeChecking/Rewriting.hs-boot | 2 +-
.../Agda/TypeChecking/Rewriting/NonLinMatch.hs | 281 +
src/full/Agda/TypeChecking/Rules/Builtin.hs | 86 +-
.../Agda/TypeChecking/Rules/Builtin/Coinduction.hs | 48 +-
src/full/Agda/TypeChecking/Rules/Data.hs | 28 +-
src/full/Agda/TypeChecking/Rules/Decl.hs | 286 +-
src/full/Agda/TypeChecking/Rules/Def.hs | 588 +-
src/full/Agda/TypeChecking/Rules/Def.hs-boot | 2 +-
src/full/Agda/TypeChecking/Rules/LHS.hs | 641 ++-
src/full/Agda/TypeChecking/Rules/LHS/Implicit.hs | 78 +-
.../Agda/TypeChecking/Rules/LHS/Instantiate.hs | 4 +-
src/full/Agda/TypeChecking/Rules/LHS/Problem.hs | 26 +-
.../Agda/TypeChecking/Rules/LHS/ProblemRest.hs | 9 +-
src/full/Agda/TypeChecking/Rules/LHS/Split.hs | 196 +-
src/full/Agda/TypeChecking/Rules/LHS/Unify.hs | 182 +-
src/full/Agda/TypeChecking/Rules/Record.hs | 239 +-
src/full/Agda/TypeChecking/Rules/Term.hs | 543 +-
src/full/Agda/TypeChecking/Rules/Term.hs-boot | 6 +-
src/full/Agda/TypeChecking/Serialise.hs | 1659 +-----
src/full/Agda/TypeChecking/Serialise/Base.hs | 640 +++
src/full/Agda/TypeChecking/Serialise/Instances.hs | 19 +
.../TypeChecking/Serialise/Instances/Abstract.hs | 279 +
.../TypeChecking/Serialise/Instances/Common.hs | 437 ++
.../TypeChecking/Serialise/Instances/Compilers.hs | 126 +
.../Serialise/Instances/Highlighting.hs | 93 +
.../TypeChecking/Serialise/Instances/Internal.hs | 418 ++
src/full/Agda/TypeChecking/SizedTypes.hs | 231 +-
src/full/Agda/TypeChecking/SizedTypes/Solve.hs | 87 +-
src/full/Agda/TypeChecking/SizedTypes/Syntax.hs | 41 +-
src/full/Agda/TypeChecking/SizedTypes/Tests.hs | 19 +-
src/full/Agda/TypeChecking/SizedTypes/Utils.hs | 3 +
.../Agda/TypeChecking/SizedTypes/WarshallSolver.hs | 116 +-
src/full/Agda/TypeChecking/Substitute.hs | 290 +-
src/full/Agda/TypeChecking/SyntacticEquality.hs | 16 +-
src/full/Agda/TypeChecking/Telescope.hs | 61 +-
src/full/Agda/TypeChecking/Test/Generators.hs | 11 +-
src/full/Agda/TypeChecking/Unquote.hs | 13 +-
src/full/Agda/TypeChecking/With.hs | 681 ++-
src/full/Agda/Utils/AssocList.hs | 2 +-
src/full/Agda/Utils/Bag.hs | 15 +-
src/full/Agda/Utils/Benchmark.hs | 165 +
src/full/Agda/Utils/BiMap.hs | 12 +-
src/full/Agda/Utils/Cluster.hs | 6 +-
src/full/Agda/Utils/Either.hs | 34 +-
src/full/Agda/Utils/Empty.hs | 2 +-
src/full/Agda/Utils/Except.hs | 26 +-
src/full/Agda/Utils/Favorites.hs | 31 +-
src/full/Agda/Utils/FileName.hs | 14 +-
src/full/Agda/Utils/Function.hs | 14 +
src/full/Agda/Utils/Functor.hs | 22 +-
src/full/Agda/Utils/Graph/AdjacencyMap.hs | 390 --
.../Utils/Graph/AdjacencyMap/Unidirectional.hs | 609 +-
.../Graph/AdjacencyMap/Unidirectional/Tests.hs | 372 ++
src/full/Agda/Utils/HashMap.hs | 26 +-
src/full/Agda/Utils/IORef.hs | 14 +-
src/full/Agda/Utils/Impossible.hs | 2 +-
src/full/Agda/Utils/Lens.hs | 23 +-
src/full/Agda/Utils/Lens/Examples.hs | 2 +-
src/full/Agda/Utils/List.hs | 29 +-
src/full/Agda/Utils/ListT.hs | 148 +
src/full/Agda/Utils/ListT/Tests.hs | 48 +
src/full/Agda/Utils/Maybe.hs | 48 +-
src/full/Agda/Utils/Maybe/Strict.hs | 24 +-
src/full/Agda/Utils/Monad.hs | 31 +-
src/full/Agda/Utils/Null.hs | 52 +-
src/full/Agda/Utils/PartialOrd.hs | 12 +-
src/full/Agda/Utils/Permutation.hs | 60 +-
src/full/Agda/Utils/Permutation/Tests.hs | 18 +-
src/full/Agda/Utils/Pointed.hs | 19 -
src/full/Agda/Utils/Pointer.hs | 4 +-
src/full/Agda/Utils/Pretty.hs | 46 +-
src/full/Agda/Utils/ReadP.hs | 23 +-
src/full/Agda/Utils/SemiRing.hs | 17 +
src/full/Agda/Utils/Singleton.hs | 73 +
src/full/Agda/Utils/Size.hs | 19 +-
src/full/Agda/Utils/String.hs | 24 +-
src/full/Agda/Utils/Suffix.hs | 2 +-
src/full/Agda/Utils/Time.hs | 41 +-
src/full/Agda/Utils/Trie.hs | 23 +-
src/full/Agda/Utils/Tuple.hs | 8 +-
src/full/Agda/Utils/VarSet.hs | 6 -
src/full/Agda/Utils/Warshall.hs | 17 +-
252 files changed, 18922 insertions(+), 18630 deletions(-)
delete mode 100644 debian/patches/0001-.cabal-Supporting-only-cpphs-1.19.patch
delete mode 100644 debian/patches/hashtables-dep
delete mode 100644 debian/patches/series
delete mode 100644 dist/build/Agda/Syntax/Parser/Lexer.hs
delete mode 100644 dist/build/Agda/Syntax/Parser/Parser.hs
delete mode 100644 src/data/EpicInclude/AgdaPrelude.e
delete mode 100644 src/data/EpicInclude/stdagda.c
delete mode 100644 src/data/EpicInclude/stdagda.h
create mode 100644 src/full/Agda/Benchmarking.hs
rename src/full/Agda/Interaction/{CommandLine => }/CommandLine.hs (92%)
create mode 100644 src/full/Agda/Interaction/InteractionTop.hs-boot
delete mode 100644 src/full/Agda/Interaction/Response.hs-boot
create mode 100644 src/full/Agda/Syntax/Fixity.hs-boot
create mode 100644 src/full/Agda/TypeChecking/Free/Lazy.hs
copy src/full/Agda/TypeChecking/{Free.hs => Free/Old.hs} (97%)
create mode 100644 src/full/Agda/TypeChecking/Free/Tests.hs
delete mode 100644 src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs
delete mode 100644 src/full/Agda/TypeChecking/Monad/Base/KillRange.hs
delete mode 100644 src/full/Agda/TypeChecking/Monad/Debug.hs
create mode 100644 src/full/Agda/TypeChecking/Positivity/Occurrence.hs
create mode 100644 src/full/Agda/TypeChecking/Positivity/Tests.hs
create mode 100644 src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Base.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances/Abstract.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances/Compilers.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances/Highlighting.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs
create mode 100644 src/full/Agda/Utils/Benchmark.hs
delete mode 100644 src/full/Agda/Utils/Graph/AdjacencyMap.hs
create mode 100644 src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional/Tests.hs
create mode 100644 src/full/Agda/Utils/ListT.hs
create mode 100644 src/full/Agda/Utils/ListT/Tests.hs
delete mode 100644 src/full/Agda/Utils/Pointed.hs
create mode 100644 src/full/Agda/Utils/Singleton.hs
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-haskell/agda.git
More information about the Pkg-haskell-commits
mailing list