aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-05-26Merge PR #10220: Use new coqrst syntax for alternatives in SSReflect chapter.Enrico Tassi
2019-05-26More precise type for Safe_typing export and inlining of private constants.Pierre-Marie Pédrot
2019-05-26Code sharing inside Cooking.Pierre-Marie Pédrot
2019-05-26Actually merge Discharge into Cooking.Pierre-Marie Pédrot
2019-05-26Share API between Discharge and Cooking.Pierre-Marie Pédrot
2019-05-26Move the Discharge module into the kernel.Pierre-Marie Pédrot
2019-05-25Merge PR #10244: Coqc: Treat unknown arguments starting with dash as unknown ...Emilio Jesus Gallego Arias
2019-05-25Merge PR #9288: Giving preference to syntax "injection ... as [= pat1 ... pat...Théo Zimmermann
2019-05-25Coqc: Treat unknown arguments starting with dash as unknown options rather th...Hugo Herbelin
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
2019-05-25Centralize the hashconsing of constant declarations.Pierre-Marie Pédrot
2019-05-24Add SUPPORT.md file.Théo Zimmermann
2019-05-24Update README, remove MacPorts link (not updated since 8.8.2).Théo Zimmermann
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-24Use global env in numeral and string notationsMaxime Dénès
2019-05-24Stop using pstate in global print queriesGaëtan Gilbert
2019-05-24Merge PR #10209: Fix #10208 don't fail when passed extensionless -topfileEnrico Tassi
2019-05-24Update coqdev-setup-proofgeneral for duneGaëtan Gilbert
2019-05-24Merge PR #10201: Remove access to indirect opaques in the kernelEnrico Tassi
2019-05-24Merge PR #10163: Fix dependencies of new test file and fix macOS issues.Vincent Laporte
2019-05-24Adding overlays.Pierre-Marie Pédrot
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-24Move body_of_constant_body to Global and specialize its uses.Pierre-Marie Pédrot
2019-05-24Statically ensure the content of delayed proofs in vio file.Pierre-Marie Pédrot
2019-05-24Remove a useless call to the Future API for opaque proofs in the STM.Pierre-Marie Pédrot
2019-05-24Remove a last use of opacity-piercing function in Safe_typing.Pierre-Marie Pédrot
2019-05-24Fixing typosJPR
2019-05-23Merge PR #10118: Make progress toward #9411: reject new undefined references.Clément Pit-Claudel
2019-05-24Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}`Emilio Jesus Gallego Arias
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 3JPR
2019-05-23Make progress toward #9411: reject new undefined references.Théo Zimmermann
2019-05-23Merge PR #10195: Minor Ltac2 documentation fix: type parameters are optional.Clément Pit-Claudel
2019-05-23Merge PR #10217: Less undefined tokensClément Pit-Claudel
2019-05-23Merge PR #10227: Update `Bind Scope` documentation to reflect dynamic binding...Théo Zimmermann
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-23Suggestions from review.Théo Zimmermann
2019-05-23Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ...Maxime Dénès
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
2019-05-23More misc refman fixes, less undefined tokens.Théo Zimmermann
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
2019-05-23Use new coqrst syntax for alternatives in SSReflect chapter.Théo Zimmermann
2019-05-23Update `Bind Scope` documentation to reflect 3d09e39dd423d81c6af3e991d5b282ea...Maxime Dénès
2019-05-23Merge PR #10221: Fixing typos - Part 2 (reopening of #10218)Théo Zimmermann
2019-05-23Merge PR #10192: More miscellaneous refman fixes (reopened version of #10187)Théo Zimmermann
2019-05-23Merge PR #10214: Better dune ocamldebug integrationEmilio Jesus Gallego Arias
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 17:10:40 +0000