aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-04-25Merge PR #13674: Enhance the performance of the move tacticHEADmastercoqbot-app[bot]
2021-04-23Merge PR #14075: New level of abstraction for streams with (non-canonical) lo...Pierre-Marie Pédrot
2021-04-23Merge PR #14158: Provide a reinit data for Ltac2 notations with entry level 4.coqbot-app[bot]
2021-04-23Merge PR #14041: Enable canonical fun _ => _ projections.coqbot-app[bot]
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
2021-04-23Merge PR #14161: test-suite: add approve-coqdoc to update all coqdoc output f...coqbot-app[bot]
2021-04-23Overlay for elpi.Hugo Herbelin
2021-04-23Relying on the abstract notion of streams with location for parsing.Hugo Herbelin
2021-04-23Locations: Moving functions Ploc.sub and Ploc.after to loc.ml.Hugo Herbelin
2021-04-23LStream: a library for streams with non-canonical locations.Hugo Herbelin
2021-04-23Gramlib: token_ematch has a useless argument.Hugo Herbelin
2021-04-23test-suite: add approve-coqdoc to update all coqdoc output files at once.Hugo Herbelin
2021-04-23Provide a reinit data for Ltac2 notations with entry level 4.Pierre-Marie Pédrot
2021-04-22Merge PR #14128: Uniformize the name of the Ltac2 boolean equality function.coqbot-app[bot]
2021-04-22Merge PR #14143: Add mczify to CIcoqbot-app[bot]
2021-04-22Add changelogPierre Roux
2021-04-22Extend Canonical Structure documentation.Jan-Oliver Kaiser
2021-04-22Enable canonical `fun _ => _` projections.Jan-Oliver Kaiser
2021-04-21Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.coqbot-app[bot]
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
2021-04-21Add mczify to CIKazuhiko Sakaguchi
2021-04-20Merge PR #14133: Slightly tweak the not-unit Ltac2 warning.coqbot-app[bot]
2021-04-20Merge PR #14131: Check for existence before using `Global.lookup_constant` in...Pierre-Marie Pédrot
2021-04-20More efficient variable membership check for Logic.move.Pierre-Marie Pédrot
2021-04-20Do not construct intermediate lists in Logic.move.Pierre-Marie Pédrot
2021-04-20Specialize the code of Logic.move.Pierre-Marie Pédrot
2021-04-20Preserve the context_val structure as much as possible in Logic.move.Pierre-Marie Pédrot
2021-04-20Merge PR #14089: unify for Ltac2Pierre-Marie Pédrot
2021-04-19Merge PR #14068: [build] Remove leftovers of code signing / OSX IDE infrastru...coqbot-app[bot]
2021-04-19changelog entry for Ltac2 unifySamuel Gruetter
2021-04-19Merge PR #14060: Coqide: on MacOS X, allow the command (⌘) key to be set/un...Pierre-Marie Pédrot
2021-04-19[build] Remove leftovers of codesigning / OSX IDe infrastructure.Emilio Jesus Gallego Arias
2021-04-19Merge PR #14108: [zify] bugfixVincent Laporte
2021-04-19Check for existence before using `Global.lookup_constant` instead of catching...Lasse Blaauwbroek
2021-04-19Slightly tweak the not-unit Ltac2 warning.Pierre-Marie Pédrot
2021-04-19Merge PR #13846: Include (* ... *) comments in .. coqtop:: directives in Sphi...coqbot-app[bot]
2021-04-19Merge PR #13815: Improve description of conversionscoqbot-app[bot]
2021-04-18Coqide: on MacOS X, allow the command key to be set/unset as a modifier.Hugo Herbelin
2021-04-18Merge PR #14122: Remove macOS dmg build.coqbot-app[bot]
2021-04-18Merge PR #14115: Change `Coqlib.lib_ref` to fail with `NameNotRegistered` ins...coqbot-app[bot]
2021-04-18Merge PR #14127: Pin docutils to 0.16.coqbot-app[bot]
2021-04-18Merge PR #14112: Cleanup useless environment manipulation in Class declarationcoqbot-app[bot]
2021-04-17Uniformize the name of the Ltac2 boolean equality function.Pierre-Marie Pédrot
2021-04-17Improve conversion chapter.Jim Fehrle
2021-04-17Disambiguate move tactics.Jim Fehrle
2021-04-17Include (* ... *) comments in .. coqtop:: directives in Sphinx outputJim Fehrle
2021-04-17Pin docutils to 0.16.Théo Zimmermann
2021-04-17Remove superfluous sort.Jim Fehrle
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
2021-04-16[zify] bugfixFrederic Besson