aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
2019-06-12Merge PR #10358: [docker] update elpi to 1.3.1Gaëtan Gilbert
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-11overlayEnrico Tassi
2019-06-11Adding an overlay for Equations.Pierre-Marie Pédrot
2019-06-11update elpi to 1.3.1Enrico Tassi
2019-06-10[ci] [fiat-crypto] Enable more targets on Coq CIJason Gross
2019-06-09[ci] Overlays for move_termination_routine_outEmilio 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-08Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq.Hugo Herbelin
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-07Merge PR #10236: Update coqdev-setup-proofgeneral for duneEmilio Jesus Gallego Arias
2019-06-07simple IO CI branch is now `master`Gaëtan Gilbert
2019-06-06CI: Test ml compilation of each commit in a PR in lint jobGaëtan Gilbert
2019-06-06Remove old overlaysGaëtan Gilbert
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ...Gaëtan Gilbert
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-06-04update overlaysEnrico Tassi
2019-06-04VernacExtend produces vernac_interp_phase ADT (old name functional_vernac)Gaëtan Gilbert
2019-06-04Overlays for coq/coq#10050 (proof_global API changes)Gaëtan Gilbert
2019-06-04Vernacextend only returns a proof_global.t option, not a vernacstateGaëtan Gilbert
2019-06-01Adding overlay for elpiHugo Herbelin
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-28Fix [Drop. #use "include";;] for indirect_accessorGaëtan Gilbert
2019-05-27Overlay for mind_kelim change (#10133)Gaëtan Gilbert
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-24Update coqdev-setup-proofgeneral for duneGaëtan Gilbert
2019-05-24Adding overlays.Pierre-Marie Pédrot
2019-05-23Fixing typos - Part 3JPR
2019-05-23Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ...Maxime Dénès
2019-05-23Merge PR #10221: Fixing typos - Part 2 (reopening of #10218)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
2019-05-23Fixing typos - Part 2JPR
2019-05-22Better dune ocamldebug integrationGaëtan Gilbert
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based generalizatio...Hugo Herbelin
2019-05-22Update build-system.txtFourchaux
2019-05-21Fixing typos - Part 1JPR
2019-05-21[loadpath] Further cleanup after merge with MlTop.Emilio Jesus Gallego Arias
2019-05-21Overlay for definition-not-visible overhaulGaëtan Gilbert
2019-05-21Overlay for removing Instance: !type syntaxGaëtan Gilbert
2019-05-17Overlay for removing Generalized 1st argGaëtan Gilbert
2019-05-17[nix] Update reference to nixpkgsVincent Laporte
2019-05-17[Nix-ci] Update Unicoq patchVincent Laporte
2019-05-17[Nix-CI] Bignums no longer depends on camlp5Vincent Laporte
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
2019-05-14Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2Pierre-Marie Pédrot
2019-05-14Merge PR #10164: Add aucontext debug printerPierre-Marie Pédrot
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot