Users' contribution for v8.4
- AACTactics
- ABP
- AILS
- AMM11262
- ATBR
- Additions
- Algebra
- Angles
- AreaMethod
- Automata
- AxiomaticABP
- BDDs
- Bertrand
- Buchberger
- CCS
- CTLTCTL
- CanonBDDs
- Cantor
- CatsInZFC
- Checker
- Chinese
- Circuits
- CoLoR
- CoRN
- Coalgebras
- CoinductiveExamples
- CoinductiveReals
- CompCert
- ConCaT
- ConstructiveGeometry
- Containers
- Continuations
- CoqInCoq
- Coqoban
- Counting
- CoursDeCoq
- Demos
- DescenteInfinie
- Dictionaries
- DistributedReferenceCounting
- DomainTheory
- Ergo
- EuclideanGeometry
- EulerFormula
- ExactRealArithmetic
- Exceptions
- FOUnify
- FSSecModel
- FSets
- Fairisle
- Fermat4
- FingerTree
- FiringSquad
- Float
- FreeGroups
- FunctionsInZFC
- FundamentalArithmetics
- GC
- GenericEnvironments
- Goedel
- GraphBasics
- Graphs
- GroupTheory
- Groups
- Hardware
- Hedges
- HighSchoolGeometry
- HigmanCF
- HigmanNW
- HigmanS
- HistoricalExamples
- HoareTut
- Huffman
- IEEE754
- IPC
- IZF
- Icharate
- IdxAssoc
- IntMap
- JProver
- JordanCurveTheorem
- Karatsuba
- Kildall
- LTL
- Lambda
- Lambek
- LinAlg
- MapleMode
- Markov
- MathClasses
- Maths
- Matrices
- Micromega
- MiniC
- MiniCompiler
- MiniML
- ModRed
- Multiplier
- MutualExclusion
- Nfix
- OrbStab
- OtwayRees
- PAutomata
- PTS
- PTSATR
- Paradoxes
- ParamPi
- PersistentUnionFind
- PiCalc
- Pocklington
- Presburger
- Prfx
- ProjectiveGeometry
- QArith
- QArithSternBrocot
- QuicksortComplexity
- RSA
- RailroadCrossing
- Ramsey
- Random
- Rational
- RecursiveDefinition
- ReflexiveFirstOrder
- RegExp
- RelationAlgebra
- RelationExtraction
- ReleasedSsreflect
- Rem
- RulerCompassGeometry
- SMC
- Schroeder
- SearchTrees
- Semantics
- Shuffle
- SquareMatrices
- Stalmarck
- Streams
- String
- Subst
- Sudoku
- SumOfTwoSquare
- Tait
- TarskiGeometry
- ThreeGap
- Topology
- TortoiseHareAlgorithm
- TreeAutomata
- TreeDiameter
- WeakUpTo
- ZChinese
- ZF
- ZFC
- ZSearchTrees
- ZornsLemma
- lazyPCF
- lc