aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2018-12-05[ci] Add four color theorem proof to CIEmilio Jesus Gallego Arias
2018-12-05Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t`Pierre-Marie Pédrot
2018-12-05Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks.Pierre-Marie Pédrot
2018-12-04CI: track dev branch of coq-simple-ioYishuai Li
2018-12-04Merge PR #8187: Notation printing based on scopes (take 2, including bug fixes)Emilio Jesus Gallego Arias
2018-12-04Merge PR #9053: Document code owner team creation.Maxime Dénès
2018-12-04Addressing issues with PR#873: performance and use of abbreviation for printing.Hugo Herbelin
We do a couple of changes: - Splitting notation keys into more categories to make table smaller. This should (a priori) make printing faster (see #6416). - Abbreviations are treated for printing like single notations: they are pushed to the scope stack, so that in a situation such as Open Scope foo_scope. Notation foo := term. Open Scope bar_scope. one looks for notations first in scope bar_scope, then try to use foo, they try for notations in scope foo_scope. - We seize the opportunity of this commit to simplify availability_of_notation which is now integrated to uninterp_notation and which does not have to be called explicitly anymore.
2018-12-03Merge PR #9112: [release doc] vX.X branches are now automatically protected.Maxime Dénès
2018-11-30[vernac] [hooks] Refactor towards optional hooks.Emilio Jesus Gallego Arias
We make `declaration_hook`s optional arguments everywhere, and thus we avoid some "fake" functions having to be passed. This identifies positively the code really using hooks [funind, rewrite, coercions, program, and canonicals] and helps moving toward some hope of reification.
2018-11-30[gramlib] Remove `Ploc.t` in favor of `Loc.t`Emilio Jesus Gallego Arias
The types are identical and we have no more reason for the split. Note the following TODOS: - discrepancy of `Ploc.after` with `CLexer.after` - discrepancy of `Ploc.comments` with `CLexer.comments` - `Ploc.dummy` vs `Loc.t option`
2018-11-30Merge PR #9102: [ltac] Remove aliases already present in the lower layers.Pierre-Marie Pédrot
2018-11-29[release doc] vX.X branches are now automatically protected.Théo Zimmermann
2018-11-29Merge PR #9054: [ci] [appveyor] Move Appveyor to OPAM 2.Maxime Dénès
2018-11-28[Windows CI] Do not build any addon if WINDOWS is not enabled_all_addons.Théo Zimmermann
Co-authored-by: Michael Soegtrop <michael.soegtrop@intel.com>
2018-11-28[ltac] Remove aliases already present in the lower layers.Emilio Jesus Gallego Arias
We remove a few aliases present in the lower layers [`Genintern/Tactypes`] from `Tacexpr`. IMHO this enlarges the API for no good purpose, and difficults analysis.
2018-11-27[ci] [appveyor] Move Appveyor to OPAM 2.Emilio Jesus Gallego Arias
We update the Appveyor configuration so it uses OPAM 2.0, and thus it can install newer packages.
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a ↵Emilio Jesus Gallego Arias
write_function
2018-11-27Merge PR #7033: Remove obsolete files from dev/docThéo Zimmermann
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-26Merge PR #9057: [nix-ci] Add a README in dev/ci/nixThéo Zimmermann
2018-11-26Fix ocamldebug-coq for packed gramlibGaëtan Gilbert
2018-11-26[nix-ci] Add a README in dev/ci/nixVincent Laporte
2018-11-26[nix-ci] Use master version of UnicoqVincent Laporte
2018-11-24Merge PR #8933: Make initial evar map argument to check_evars_are_solved ↵Pierre-Marie Pédrot
optional.
2018-11-24Apply suggestions from code review Théo Zimmermann
Thanks to @Zimmi48 as always for the careful review. Co-Authored-By: ejgallego <e+git@x80.org>
2018-11-24[ci] [doc] Note about `overlay-maintainers` team.Emilio Jesus Gallego Arias
2018-11-24[ci] [doc] Note about `create-overlays.sh`Emilio Jesus Gallego Arias
2018-11-24[ci] [doc] Split user/developer README, add info about Nix/Docker CIEmilio Jesus Gallego Arias
2018-11-23Merge PR #9055: [dev] fix create_overlay wrt branch names containing /Emilio Jesus Gallego Arias
2018-11-23Merge PR #9044: Remove pidetop from CIEmilio Jesus Gallego Arias
2018-11-23Adding overlay.Pierre-Marie Pédrot
2018-11-23Overlay for private polymorphic universesGaëtan Gilbert
2018-11-23Merge PR #9021: merge-pr: Improve overlay checkMaxime Dénès
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-22[dev] fix create_overlay wrt branch names containing /Enrico Tassi
2018-11-22Document code owner team creation.Théo Zimmermann
2018-11-21Remove pidetop from CIMaxime Dénès
pidetop relies on some rather low level API from STM, which we'd like to change. It does not seem maintained much anymore, and still hasn't moved to github.
2018-11-21[camlp5] Remove dependency on camlp5.Emilio Jesus Gallego Arias
2018-11-21Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlibEnrico Tassi
2018-11-21Add overlay for solve-remaining-evars-initial-argGaëtan Gilbert
2018-11-21Merge PR #8961: dune: link kernel in checker instead of copying filesPierre-Marie Pédrot
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
We remove the `Proof_types` file which was a trivial stub, we also cleanup a few layers of aliases. This is not a lot but every little step helps.
2018-11-21[gramlib] [build] Switch make-based system to packed gramlibEmilio Jesus Gallego Arias
This makes the make-based build system stop linking to Camlp5's gramlib and instead links to our own gramlib. We use the style done in the packing of `Stdlib` in OCaml 4.07. As to introduce a minimal amount of noise in history we use an autogenerated `gramlib__pack` directory. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2018-11-20Merge PR #8948: [dune] Some tweaks to docs.Théo Zimmermann
2018-11-20[dune] Only build printers when the ltac plugin is available.Emilio Jesus Gallego Arias
This fixes a problem reported by @Zimmi48 in #8948, IMHO we should be able to have a clean build of core Coq.
2018-11-20gitlab: Install stdlib doc in build:baseGaëtan Gilbert
Looks like we forgot to adapt this when we split off the sphinx job and stopped using -with-doc yes.
2018-11-20Fix dune-dbg using checker/main -> checker/coqchkGaëtan Gilbert
2018-11-20Merge PR #7925: Clean transparent stateMaxime Dénès
2018-11-19Merge PR #9003: [vernacextend] Consolidate extension points APIPierre-Marie Pédrot
2018-11-19Merge PR #8902: [ltac] Use CAst nodes in the tactic AST.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 17:37:19 +0000