aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-07-21Merge PR #12714: [declare] Remove some dead code in declare_mutual_definitionGaë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-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-17Wording improvements.Théo Zimmermann
2020-07-17CI: pass -silent to coqchk in compcert jobGaëtan Gilbert
2020-07-17CI: Use bundled compcert for VSTGaëtan Gilbert
2020-07-16[gramlib] Remove legacy located exception wrapper in favor of standard infras...Emilio Jesus Gallego Arias
2020-07-16Merge PR #12677: Fix #12513: coq no longer reports mismatched version numbers.Emilio Jesus Gallego Arias
2020-07-16Merge PR #12675: Don't catch anomalies for evarconv "cannot find an instance"...Emilio Jesus Gallego Arias
2020-07-15Do not print global refs as terms when asked to be printed as themselves.Hugo Herbelin
2020-07-15Fix bug #12691 (an only parsing notation induces a generic printing format).Hugo Herbelin
2020-07-15[search] Don't use ad-hoc Dumpglob table for SearchEmilio Jesus Gallego Arias
2020-07-15Merge PR #12671: Minor improvement to CI logsEmilio Jesus Gallego Arias
2020-07-15Merge PR #12673: Fix fiat_crypto(_ocaml) needs/dependenciesEmilio Jesus Gallego Arias
2020-07-15Merge PR #12692: Compatibility of make-change-log with MacOS X whose "sed" do...Emilio Jesus Gallego Arias
2020-07-15Compatibility of make-change-log with MacOS X whose "sed" does not support "\+".Hugo Herbelin
2020-07-13Advertise switch to maintainer teams and credit maintainers.Théo Zimmermann
2020-07-13Merge PR #12681: tactics.rst: `Require A` is enough for `A`'s hintsThéo Zimmermann
2020-07-13Don't catch anomalies for evarconv "cannot find an instance" errorGaëtan Gilbert
2020-07-12Adding change log.Hugo Herbelin
2020-07-12Fixes #12682 (recursive notation printing bug with n-ary applications).Hugo Herbelin
2020-07-11tactics.rst: `Require A` is enough for `A`'s hintsPaolo G. Giarrusso
2020-07-11Merge PR #12650: Recordops: unify struc_typ summary record and libobject entr...Pierre-Marie Pédrot
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-Marie Pédrot
2020-07-11Merge PR #12635: Correct comment and clarify constantPierre-Marie Pédrot
2020-07-10Merge PR #12638: Some changes of representation in TacredEnrico Tassi
2020-07-10Add changelog.Pierre-Marie Pédrot
2020-07-10Fix #12513: coq no longer reports mismatched version numbers.Pierre-Marie Pédrot
2020-07-10Minor improvement to CI logsGaëtan Gilbert
2020-07-10Merge PR #12666: Add test for #10890 derive vs abstractEmilio Jesus Gallego Arias
2020-07-10Fix fiat_crypto(_ocaml) needs/dependenciesGaëtan Gilbert
2020-07-10Merge PR #12537: Take into account the existing delta-resolver when starting ...Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 07:15:35 +0000