aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-07-26Merge PR #12726: Clarify Global.env usage in ppvernacPierre-Marie Pédrot
2020-07-26Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque Define...Pierre-Marie Pédrot
2020-07-25Faster algorithm to compute algebraic universe mapping in mimization.Pierre-Marie Pédrot
2020-07-24Adding change log for #12754.Hugo Herbelin
2020-07-24Fixes #12752 (applying symbol escaping in index produced by coqdoc).Hugo Herbelin
2020-07-24Fixes reduction effect printing in the presence of non purely applicative sta...Hugo Herbelin
2020-07-24Merge PR #12747: Fix coqdoc bad bulleting from incorrect space countEmilio Jesus Gallego Arias
2020-07-24CI metacoq: make .merlinGaëtan Gilbert
2020-07-24Fix coqdoc bad bulleting from incorrect space countGaëtan Gilbert
2020-07-23Merge PR #12739: [changelog] Fix hanging changelog entry for 8.12 betaThéo Zimmermann
2020-07-23[changelog] Incorporate hanging changelog entry for 8.12+beta1Emilio Jesus Gallego Arias
2020-07-23[changelog] Fix hanging file extension.Emilio Jesus Gallego Arias
2020-07-23Merge PR #12734: [changelog] Latest changes backported to 8.12 branch.Théo Zimmermann
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-07-23Merge PR #12678: Tweak the warning for arbitrary term hints.Emilio Jesus Gallego Arias
2020-07-23Hint Opaque/Transparent/Unfold: don't error on opaque constantsGaëtan Gilbert
2020-07-23Merge PR #12672: Fix failing macOS build.Gaëtan Gilbert
2020-07-23Ignore installation failure during call to brew.Théo Zimmermann
2020-07-23Merge PR #12679: Remove redundant data from VM case switch.Gaëtan Gilbert
2020-07-23Merge PR #12698: Fixing mention of `unfold` as example of tactic taking a qua...Théo Zimmermann
2020-07-22Merge PR #12715: Add Coqtail to CIGaëtan Gilbert
2020-07-22Clarify Global.env usage in ppvernacGaëtan Gilbert
2020-07-22Merge PR #12664: Turn various anomalies into regular errors in primitive decl...Pierre-Marie Pédrot
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
2020-07-21Merge PR #12714: [declare] Remove some dead code in declare_mutual_definitionGaëtan Gilbert
2020-07-21Add Coqtail to CIwhonore
2020-07-21Turn various anomalies into regular errors in primitive declaration pathGaëtan Gilbert
2020-07-21Merge PR #12697: Fix bug #12691: an only-parsing notation needs to produce a ...Emilio Jesus Gallego Arias
2020-07-20[declare] Remove some dead code in declare_mutual_definitionEmilio Jesus Gallego Arias
2020-07-20Merge PR #12712: CI: deploy make-built stdlib docEmilio Jesus Gallego Arias
2020-07-20Merge PR #12660: Fix typo in contributing guide.Emilio Jesus Gallego Arias
2020-07-20CI: deploy make-built stdlib docGaëtan Gilbert
2020-07-20Merge PR #12684: Do not print constructor and inductive types as terms when a...Gaëtan Gilbert
2020-07-19Merge PR #12680: Better location for match! pattern variables in Ltac2.Kenji Maillard
2020-07-18Clarify the Ltac2 invalid identifier message.Pierre-Marie Pédrot
2020-07-18Better location for match! pattern variables in Ltac2.Pierre-Marie Pédrot
2020-07-18Merge PR #12588: [exn] Remove some uses of printPierre-Marie Pédrot
2020-07-18Merge PR #12696: [gramlib] Remove legacy located exception wrapper in favor o...Pierre-Marie Pédrot
2020-07-18Merge PR #12708: Do not store the full environment inside ssr ast_closure_term.Enrico Tassi
2020-07-17Add a changelog.Pierre-Marie Pédrot
2020-07-17Do not store the full environment inside ssr ast_closure_term.Pierre-Marie Pédrot
2020-07-17Documenting new primitive entry evaluable_ref usable for tactic notations.Hugo Herbelin
2020-07-17Add tests for the interpretation of "unfold".Hugo Herbelin
2020-07-17Merge PR #12693: [search] Don't use ad-hoc Dumpglob table for SearchHugo Herbelin
2020-07-17Merge PR #12670: Advertise switch to maintainer teams and credit maintainers.Emilio Jesus Gallego Arias
2020-07-17Merge PR #12701: CI: Use bundled compcert for VSTEmilio Jesus Gallego Arias
2020-07-17Merge PR #12702: CI: pass -silent to coqchk in compcert jobEmilio Jesus Gallego Arias
2020-07-17Merge PR #12683: Fixes #12682: printing bug with recursive notations for n-ar...Emilio Jesus Gallego Arias
2020-07-17Merge PR #12631: Fix record pattern interpretation with implicit argumentsEmilio Jesus Gallego Arias
2020-07-17Remove automatic formatting of ComHints.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 17:43:50 +0000