aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2019-10-18Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in ↵Gaëtan Gilbert
the kernel. Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares
2019-10-17Fix link to `xml-protocol.md` in `dev/README.md`Michael D. Adams
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
Opening up a lambda should always lift the substitution attached to it.
2019-10-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
Reviewed-by: JasonGross Reviewed-by: gares Ack-by: ppedrot
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-13Doc update with mlg extension - fix #10855mcaci
2019-10-11Merge PR #10828: Simple script to prefill a changelog entryThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-11Merge PR #10850: chmod -x some filesGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2019-10-11Simple script to prefill a changelog entryGaëtan Gilbert
2019-10-08Merge PR #10840: Release process: release notesThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-08Merge PR #10770: [ci] Add mit-pdos/perennialEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-10-07chmod -x some filesJason Gross
They probably don't need to be executable
2019-10-07Release process: release notesVincent Laporte
Explain into the release process how to prepare the release notes.
2019-10-07Merge PR #9933: Add a few missing notes to the release doc.Vincent Laporte
Ack-by: ejgallego Reviewed-by: vbgl
2019-10-04overlays for sprop default onGaëtan Gilbert
2019-10-03Merge PR #10727: [library] Move `Declaremods` to `vernac/`Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: herbelin Reviewed-by: ppedrot
2019-10-02Merge PR #10768: [ci] Update to OCaml 4.09.0, drop now useless "trunk" jobs.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-09-25Adding documentation for the move of sections data to kernel.Pierre-Marie Pédrot
2019-09-20[ci] Add mit-pdos/perennialTej Chajed
2019-09-19[ci] Update supported OCaml version to 4.09.0Emilio Jesus Gallego Arias
2019-09-18[declaremods] Remove abstraction layer over module interpretation.Emilio Jesus Gallego Arias
Now that we place imperative module declaration on top of module interpretation we can remove the abstraction layer used in `Declaremods`, so the `interp_modast` parameter goes away. Improvement suggested by Gaëtan Gilbert.
2019-09-17Merge PR #10738: update elpi to 1.7Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-09-17Overlay for VSTMaxime Dénès
2019-09-16Add SF overlayMaxime Dénès
2019-09-07overlay for elpiEnrico Tassi
2019-09-07update elpi to 1.7Enrico Tassi
2019-09-02Merge PR #10645: [ci] Update to OCaml 4.08.1Gaëtan Gilbert
Ack-by: Zimmi48 Reviewed-by: vbgl Reviewed-by: SkySkimmer
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: herbelin Ack-by: mattam82 Reviewed-by: ppedrot
2019-08-30Adding a critical-bugs entry. Description from Hugo Herbelin.Pierre-Marie Pédrot
2019-08-29Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ↵Pierre-Marie Pédrot
proof data on top of declare. Reviewed-by: ppedrot
2019-08-27[ci] Update to OCaml 4.08.1Emilio Jesus Gallego Arias
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on ↵Emilio Jesus Gallego Arias
top of declare. This PR is a follow up to #10406 , moving the then introduced `proof_entry` type to `Declare`. This makes sense as `Declare` is the main consumer of the entry type, and already provides the constructors for it. This is a step towards making the entry type private, which will allow us to enforce / handle invariants on entry data better. A side-effect of this PR is that now `Proof_global` does depend on `Declare`, not the other way around, but that makes sense given that closing an interactive proof will be a client of declare. Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into tactics due to `abstract`, at some point we may be able to unify all them into a single file in `vernac`.
2019-08-27[cleanup] Replace uses of UserError constructor, clarify exception names.Emilio Jesus Gallego Arias
We replace some uses of `raise (UserError ...)` with `CErrors.user_err`, ideally we would like to make the error raising API not depend on the exception themselves, but that's still a long way to go. We also rename the `Timeout` exception as to clarify purpose in the codebase, given that it has 3 different ones as of today. cc: #7560
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-08-22[dune] Move to Dune 1.10, use coq.pp directive.Emilio Jesus Gallego Arias
We use the `(coq.pp ...)` dune directive which will produce correct error messages for `.mlg` files. Unfortunately we cannot yet use the automatic opam generation features of Dune 1.10, as this does require a fully native Dune build. Dune 1.6-1.10 has quite a few other improvements that could be used by Coq, for example for promote modes. I have fixed a couple of documentation issues. `Drop` and `ocamldebug` have been tested in this version.
2019-08-20[ci] Remove dead code.Théo Zimmermann
TLC and CPDT are not actually tested. No point in keeping them as if they were.
2019-08-19Merge PR #10672: Std++, Iris, and Lambda-Rust have moved.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
We move `binder_kind` to the pretyping AST, removing the last data type in the now orphaned file `Decl_kinds`. This seems a better fit, as this data is not relevant to the lower layers but only used in `Impargs`. We also move state keeping to `Impargs`, so now implicit declaration must include the type. We also remove a duplicated function.
2019-08-19Remove links to doc artifacts and replace them with the deployed versions.Théo Zimmermann
2019-08-19Std++, Iris, and Lambda-Rust have moved.Théo Zimmermann
We update the URLs to the new ones, even if the previous continue to work.
2019-08-09Overlay for #10642Gaëtan Gilbert
2019-07-29Fix issue #10593 : Software foundations URL changedMichael Soegtrop
2019-07-23Merge PR #10541: Dune: fix build_all_stdlib ruleEmilio Jesus Gallego Arias
Ack-by: ejgallego
2019-07-22Merge PR #10447: Refactor and expand contributing guide.Maxime Dénès
Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: jfehrle
2019-07-22Merge PR #10441: Attach the universe polymorphic status to sections.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: mattam82
2019-07-21Dune: do not use with-outputs-to for shimsGaëtan Gilbert
We only want stdout, so if there's something in stderr it will both make a wrong output and make it harder to debug.
2019-07-19Removed patches for Flocq, Interval and Gappa (merged upstream)Michael Soegtrop
2019-07-18Adding overlays.Pierre-Marie Pédrot
2019-07-17Fixed Windows patch for QuickchickMichael Soegtrop
2019-07-17Adjust VST patch to latest changes in VSTMichael Soegtrop
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 11:20:44 +0000