Page Index - rocq-prover/rocq GitHub Wiki
480 page(s) in this GitHub Wiki:
- Home
- Coq installation
- Coq official resources
- Coq informal resources
- Coq books and tutorials
- Coq development
- Coq community
- Coq libraries
- Coq plugins and tools
- Coq's logic
- Coq Wiki
- 10000th Issue Contest
- Alternative names
- Anti patterns
- ArbitraryArity
- ArithmeticExpressionParser
- AUGER_Annotations
- AUGER_Enumerates
- AUGER_ExtractionTuto
- AUGER_LinearLogic
- AUGER_Monad
- AUGER_Notations
- Basic architecture of Coq User Interfaces
- Benchmarking
- BindingRepresentation
- BreakOut 2020 11 30 Lasse
- BreakOut 2020 12 01 envs
- BreakOut 2020 12 01 Karl
- BreakOut 2020 12 02 Ali
- BreakOut 2020 12 03 MetaCoq
- BreakOut 2020 12 03 Paolo
- BugzillaVsOtherTools
- BuildingCoqOnMac
- Case Studies
- Changes in Coq since the last WG (20181022)
- Changes in Coq since the last WG (20181216)
- CleanDuplicatedHypothesis
- ComparisonWithOtherSystems
- Configuration of Coq LSP
- Configuration of CoqIDE
- Configuration of Proof General
- Coq Call 2019 09 18
- Coq Call 2019 09 25
- Coq Call 2019 10 16
- Coq Call 2019 10 23
- Coq Call 2019 11 06
- Coq Call 2019 11 13
- Coq Call 2019 11 20
- Coq Call 2019 11 27
- Coq Call 2019 12 04
- Coq Call 2019 12 11
- Coq Call 2020 01 15
- Coq Call 2020 01 22
- Coq Call 2020 01 29
- Coq Call 2020 02 05
- Coq Call 2020 02 12
- Coq Call 2020 02 19
- Coq Call 2020 02 26
- Coq Call 2020 03 04
- Coq Call 2020 03 11
- Coq Call 2020 03 18
- Coq Call 2020 03 25
- Coq Call 2020 04 01
- Coq Call 2020 04 08
- Coq Call 2020 04 22
- Coq Call 2020 04 29
- Coq Call 2020 05 13
- Coq Call 2020 05 20
- Coq Call 2020 06 03
- Coq Call 2020 06 17
- Coq Call 2020 06 24
- Coq Call 2020 07 15
- Coq Call 2020 07 22
- Coq Call 2020 09 02
- Coq Call 2020 09 09
- Coq Call 2020 09 16
- Coq Call 2020 09 23
- Coq Call 2020 10 07
- Coq Call 2020 10 21
- Coq Call 2020 10 28
- Coq Call 2020 11 04
- Coq Call 2020 11 13
- Coq Call 2020 11 18
- Coq Call 2020 11 25
- Coq Call 2020 12 09
- Coq Call 2020 12 16
- Coq Call 2021 01 13
- Coq Call 2021 01 27
- Coq Call 2021 02 03
- Coq Call 2021 02 10
- Coq Call 2021 02 17
- Coq Call 2021 02 24
- Coq Call 2021 03 03
- Coq Call 2021 03 10
- Coq Call 2021 03 17
- Coq Call 2021 03 24
- Coq Call 2021 03 31
- Coq Call 2021 04 07
- Coq Call 2021 04 21
- Coq Call 2021 04 28
- Coq Call 2021 05 05
- Coq Call 2021 05 12
- Coq Call 2021 05 19
- Coq Call 2021 05 26
- Coq Call 2021 06 16
- Coq Call 2021 06 23
- Coq Call 2021 06 30
- Coq Call 2021 07 07
- Coq Call 2021 07 13
- Coq Call 2021 09 01
- Coq Call 2021 09 08
- Coq Call 2021 09 15
- Coq Call 2021 09 22
- Coq Call 2021 09 29
- Coq Call 2021 10 13
- Coq Call 2021 10 20
- Coq Call 2021 10 27
- Coq Call 2021 11 03
- Coq Call 2021 11 10
- Coq Call 2021 11 17
- Coq Call 2021 12 01
- Coq Call 2021 12 08
- Coq Call 2021 12 15
- Coq Call 2022 01 05
- Coq Call 2022 01 12
- Coq Call 2022 01 26
- Coq Call 2022 02 02
- Coq Call 2022 02 09
- Coq Call 2022 02 23
- Coq Call 2022 03 09
- Coq Call 2022 03 16
- Coq Call 2022 04 06
- Coq Call 2022 04 13
- Coq Call 2022 04 20
- Coq Call 2022 04 27
- Coq Call 2022 05 04
- Coq Call 2022 05 11
- Coq Call 2022 05 18
- Coq Call 2022 05 25
- Coq Call 2022 06 01
- Coq Call 2022 06 29
- Coq Call 2022 08 17
- Coq Call 2022 08 31
- Coq Call 2022 09 21
- Coq Call 2022 09 28
- Coq Call 2022 10 05
- Coq Call 2022 10 12
- Coq Call 2022 10 19
- Coq Call 2022 11 02
- Coq Call 2022 11 16
- Coq Call 2022 11 30
- Coq Call 2023 01 04
- Coq Call 2023 01 11
- Coq Call 2023 01 18
- Coq Call 2023 01 25
- Coq Call 2023 02 08
- Coq Call 2023 03 01
- Coq Call 2023 03 08
- Coq Call 2023 03 28
- Coq Call 2023 04 04
- Coq Call 2023 04 25
- Coq Call 2023 05 09
- Coq Call 2023 05 16
- Coq Call 2023 05 23
- Coq Call 2023 06 06
- Coq Call 2023 07 11
- Coq Call 2023 07 18
- Coq Call 2023 08 08
- Coq Call 2023 09 05
- Coq Call 2023 09 12
- Coq Call 2023 09 19
- Coq Call 2023 09 26
- Coq Call 2023 10 03
- Coq Call 2023 10 10
- Coq Call 2023 10 24
- Coq Call 2023 10 31
- Coq Call 2023 11 07
- Coq Call 2023 11 14
- Coq Call 2023 11 21
- Coq Call 2023 12 04
- Coq Call 2023 12 11
- Coq Call 2024 01 15
- Coq Call 2024 01 22
- Coq Call 2024 01 29
- Coq Call 2024 02 05
- Coq Call 2024 02 12
- Coq Call 2024 02 19
- Coq Call 2024 03 05
- Coq Call 2024 03 19
- Coq Call 2024 03 26
- Coq Call 2024 04 02
- Coq Call 2024 04 09
- Coq Call 2024 04 23
- Coq Call 2024 04 30
- Coq Call 2024 05 07
- Coq Call 2024 05 21
- Coq Call 2024 05 28
- Coq Call 2024 06 04
- Coq Call 2024 06 11
- Coq Call 2024 08 27
- Coq Call 2024 09 10
- Coq Call 2024 09 17
- Coq Call 2024 10 01
- Coq Call 2024 10 08
- Coq Call 2024 10 22
- Coq Call 2024 10 29
- Coq Call 2024 11 05
- Coq Call 2024 11 12
- Coq Call 2024 11 19
- Coq Call 2024 12 03
- Coq Call 2024 12 10
- Coq Call 2024 12 17
- Coq Call 2025 01 07
- Coq Call 2025 01 14
- Coq Call 2025 01 21
- Coq Call 2025 01 28
- Coq Call 2025 02 25
- Coq Call 2025 03 04
- Coq Call 2025 03 11
- Coq Calls
- Coq Implementors Workshop 2018
- Coq Implementors Workshop 2018 log
- Coq Meetings Organization
- Coq Topic Working Group Document Data and Machine Learning Platform
- Coq Topic Working Group Meta Programming Rosetta Stone
- Coq Topic Working Group Multicore
- Coq Topic Working Group User Interfaces
- Coq Users and Developers Workshop 2019
- Coq Users and Developers Workshop 2020
- Coq Users and Developers Workshop 2023
- Coq Users and Developers Workshop 2024
- Coq Working Group 15 06 2022 Notes
- Coq Working Group 2019 12 16
- Coq Working Groups
- CoqAndAxioms
- Coqbot minimize feature
- CoqCodingSprint
- CoqCS1
- CoqCS1 bsp
- CoqCS1 log
- CoqDevelopment
- Coqdoc
- CoqIde configuration to input special characters
- CoqIDEWishes
- CoqImplementorsWorkshop
- CoqInTheClassroom
- CoqInTheClassroomInitial
- CoqIW2016
- CoqIW2016 log
- CoqIW2017
- CoqIW2017log
- CoqNewbieQuestions
- CoqPaths
- CoqStyle
- CoqTerminationDiscussion
- CoqWG 2018 10 22
- CoqWG 2018 12 19
- CoqWG 2019 02 06
- CoqWG 2019 10
- CoqWG 2020 05 04
- CoqWG 2022 02
- CoqWG 2022 06 15
- CoqWG 2023 01 31
- CoqWG 2023‐12‐18
- CoqWG Activity
- CoqWG20140131
- CoqWG20140404
- CoqWG20140606
- CoqWG20140905
- CoqWG20141023
- CoqWG20150106
- CoqWG20150324
- CoqWG20150512
- CoqWG20150708
- CoqWG20150915
- CoqWG20151125
- CoqWG20160216
- CoqWG20160415
- CoqWG20160531
- CoqWG20160928
- CoqWG20161214
- CoqWG20170306
- CoqWG20170523
- CoqWG20171003
- CoqWG20171218
- CoqWG20180226
- CoqWG20180516
- Core Team
- Core Team Voting Process
- CoRN
- CRADT20090324
- CRADT20090630
- CRADT20100202
- CRADTCommunication20090323
- Create a CoqIDE bundle on macOS
- CRGTCoq20081010
- CRGTCoq20081118
- CRGTCoq20090116
- CRGTCoq20090323
- CRGTCoq20090704
- CRGTCoq20091103
- CRGTCoq20100113
- CRGTCoq20100426
- CRGTCoq20100920
- CRGTCoq20101217
- CRGTCoq20110414
- CRGTCoq20110706
- CRGTCoq20120119
- CRGTCoq20120920
- CRGTCoq20130214
- CRGTCoq20130709
- CRGTCoq20131126
- Default Locality Behavior of Commands
- DependentInversion
- DesignNewTacticLanguage
- Development questions
- DevelopmentArchive
- DevelopmentTutorial
- DevelSetup
- Discourse
- Discussion_on_content_and_structure_of_Cocorico!
- Documentation
- Dune WG 2024
- DuneWG 2022
- Eqdep_dec_Type
- Equality
- EqualityFreeInversion
- evar_match
- ExcludedMiddleOnNegativeFormulasFromCoqRealAxioms
- ExistentialVariablesInEapply
- ExistsFromPropToSet
- extensional_equality
- Extraction
- ExtractionNameTricks
- FixpointFiniteTypes
- Flexible status of parameters in mutual inductive types
- Folding tactics
- FormalizedAndVerified
- Future plans
- GenericTactics
- Getting Started
- Glossary
- GoogleSummerOfCode
- GTReification
- GuardConditionProblem
- GUIWishes
- HandMul
- HelpOnGithubWiki
- HourOfCoq
- HowToContributeToTheStandardLibrary
- HowToRebase
- Implications of changing the name
- Impredicative Set
- Induction over a type containing pairs
- Induction with self defined cases
- Inductive and Co Inductive Types
- InductiveFiniteTypes
- Installation
- Installation of Coq
- Installation of Coq on Linux
- Installation of Coq on Mac
- Installation of Coq on Windows
- InTac
- IntensionalEquality
- IteratedFiniteTypes
- jsCoq and CoqDB Working Day
- LagrangesTheorem
- LhsRhsTactic
- LinearTactics
- List of Coq Math Projects
- List of Coq PL Projects
- ListComprehensionNotation
- ListOfPredecessors
- Ltac
- Ltac Debugger Preview
- LtacPearls
- Marketing and Branding
- MatchAsInReturn
- MathClasses
- MigrationGit
- ModulesBibliography
- ModulesForTheories
- ModulesNotRecords
- ModuleSystem
- ModuleSystemTutorial
- Multiple Universe Hierarchies
- Mutual Induction
- Nix
- NonInductiveProps
- Notes on side effects, universes and proof closing
- Notes on the release process of Coq 8.10
- Notes on the release process of Coq 8.11
- OCaml Performance Numbers
- OCamldebug
- On the radio button "Approve" in pull requests reviewing
- OPAM
- OpenIssuesWithModules
- Other Coq Resources
- OtherContents
- Performance
- Performance experiments
- Plugin Developer Program
- PortingToCoqV8.7
- Presentation
- ProfilingCoq
- ProjectIdeas
- Proof General Error Color
- Proof General Missing Proof State
- ProofTermsConsideredHarmful
- Prop_or_Set
- PropsGuardingIotaReduction
- Public
- Published Works
- Publishing Tools
- Quick Reference for Beginners
- QuickSort
- RaccourcisPourDevelopperSousEmacs
- RecordsNotModules
- Reduction Strategies and Evaluation Order
- ReflectionOnStandardLibrary
- Refman improvements in 8.12 and beyond
- RegressionTest
- Release Plan
- Release Plan for Coq 8.11
- Release Plan for Coq 8.12
- Release Schedule for Coq 8.13
- Release Schedule for Coq 8.14
- Release Schedule for Coq 8.15
- Release Schedule for Coq 8.16
- Release Schedule for Coq 8.17
- Release Schedule for Coq 8.18
- Release Schedule for Coq 8.19
- Release Schedule for Coq 8.20
- Release Schedule for Rocq 9.0
- Remote Collaborative Editing of Coq Files
- RingTactics
- Roadmap86
- Roadmap87
- Roadmaps
- Rocq Call 2025 03 25
- Rocq Calls
- Rocq'n'code 2025
- Setoids
- SourceTreeGuide
- SquareRootTwo
- StandardLibrary
- Starter Exercises for Learning Coq
- State of the continuous integration infrastructure
- Syntax and Notations
- Tactic IfThenElse
- TacticExts
- Tactics Written in OCaml
- Talkin' with the Rooster
- TeXInputMethodForUnicodeNotations
- The Logic of Coq
- The Rocq FAQ
- TheoryBehindCoq
- Tools
- Top100MathematicalTheorems
- Top100MathematicalTheoremsInCoq
- Topic Working Groups
- Troubleshooting
- Typeclasses and Canonical Structures
- UnfoldFixpointOnce
- UnificationProblems
- Universities teaching Coq
- UntypedLambdaTerms
- Use counts for parser productions
- UsersDiscussion88
- UsersDiscussion89
- VerifyingReleases
- What to expect of a standard library about lists?
- WikiMigration
- Wishes
- Wishes for Camlp5
- WTypeInsteadOfInductiveTypes
- WtypesInCoq
- XCompose_symbols
- XComposeAndNotations
- ZInterfacePackage