aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-15[dune] Install .byte version of coqidetop like for coqtop.Théo Zimmermann
2019-06-15Merge PR #10377: Rename expr and tacexpr tokens into ltac_expr token family.Clément Pit-Claudel
2019-06-15Rename expr and tacexpr tokens into ltac_expr token family.Théo Zimmermann
2019-06-14Merge PR #10376: Add a comment documenting what fontsupport.py is.Clément Pit-Claudel
2019-06-14Add a comment documenting what fontsupport.py is.Théo Zimmermann
2019-06-14Merge PR #10322: Update changes.rst as a follow-up to #9743Théo Zimmermann
2019-06-13Merge PR #10374: Integrate 8.9.0 and 8.9.1 changelog entries.Clément Pit-Claudel
2019-06-13Merge PR #10373: Add missing changelog entry for #10360.Clément Pit-Claudel
2019-06-13Integrate 8.9.0 and 8.9.1 changelog entries.Théo Zimmermann
2019-06-13Add missing changelog entry for #10360.Théo Zimmermann
2019-06-13Update, expand, and document plugin tutorial 2Talia Ringer
2019-06-13Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLaterEnrico Tassi
2019-06-13Merge PR #10360: Resolve #9885 CoqIDE does not work on WindowsEmilio Jesus Gallego Arias
2019-06-12Merge PR #10310: Fix #10283: clearer dependency documentation for building Co...Clément Pit-Claudel
2019-06-12[funind] Untabify; necessary to ease the review of subsequent work.Emilio Jesus Gallego Arias
2019-06-12Merge PR #10358: [docker] update elpi to 1.3.1Gaëtan Gilbert
2019-06-12Remove dependency of native_compile on global env for symbolsGaëtan Gilbert
2019-06-12Merge PR #10329: Update changelog for 10302 and 10305Théo Zimmermann
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-12Fix #9455: avoid update_global_env when unchanged Global.universes()Gaëtan Gilbert
2019-06-12Merge PR #10334: Remove the side-effect role from the kernel.Enrico Tassi
2019-06-11overlayEnrico Tassi
2019-06-11Adding an overlay for Equations.Pierre-Marie Pédrot
2019-06-11Move the side-effect role out of Entries into Evd.Pierre-Marie Pédrot
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-11Merge PR #10354: [ci] [fiat-crypto] Enable more targets on Coq CIEmilio Jesus Gallego Arias
2019-06-11Resolve #9885 CoqIDE does not work on WindowsMichael Soegtrop
2019-06-11Move type definition Nativecode.symbols to NativevaluesGaëtan Gilbert
2019-06-11Overlays for 10319Gaëtan Gilbert
2019-06-11STM: encode in static types that vernac_when is only used when VtSideffGaëtan Gilbert
2019-06-11Fix #10225 (Instance := {} accepts duplicate fields)Gaëtan Gilbert
2019-06-11Simplify implicit_quantifiersGaëtan Gilbert
2019-06-11update elpi to 1.3.1Enrico Tassi
2019-06-10[ci] [fiat-crypto] Enable more targets on Coq CIJason Gross
2019-06-10Merge PR #9566: [proof] Move proofs that have an associated constant to `Lemmas`Pierre-Marie Pédrot
2019-06-09Merge PR #10325: Fix panel behavior as requested by #10292Pierre-Marie Pédrot
2019-06-09[ci] Overlays for move_termination_routine_outEmilio Jesus Gallego Arias
2019-06-09[proof] Uniformize Proof_global APIEmilio Jesus Gallego Arias
2019-06-09[save_proof] Make terminator API internal.Emilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-09Merge PR #8726: More robust treatment of the Discharge statusPierre-Marie Pédrot
2019-06-09Merge PR #10309: CI: Test ml compilation of each commit in a PR in lint jobEmilio Jesus Gallego Arias
2019-06-09Merge PR #10245: Command line: adding variants for Require, aligning on the v...Emilio Jesus Gallego Arias
2019-06-08Merge PR #10318: Test goal range in "only" selectorsPierre-Marie Pédrot
2019-06-08Merge PR #10263: [proofs] Remove unused API [detected by coverage]Pierre-Marie Pédrot
2019-06-08Fix #10339: Anomaly in Ltac2.Pierre-Marie Pédrot
2019-06-08[Test-suite] Add non-regression test case for #8725Vincent Laporte
2019-06-08Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq.Hugo Herbelin
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-08Adding a new kind of assumption to track assumption coming from "Context".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 07:37:26 +0000