aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-27Merge PR #8986: Put -indices-matter in typing_flagsMaxime Dénès
2018-11-27Merge PR #8686: [toplevel] Move compilation-related functions to their own ↵Pierre-Marie Pédrot
module.
2018-11-26Merge PR #9075: [ci] Set windows jobs to allow_failure: trueGaëtan Gilbert
2018-11-26Merge PR #9057: [nix-ci] Add a README in dev/ci/nixThéo Zimmermann
2018-11-26Merge PR #9063: [checker] Remove duplicated code from checker / clibPierre-Marie Pédrot
2018-11-26[ci] Set windows jobs to allow_failure: trueEmilio Jesus Gallego Arias
Windows jobs have been polluting the CI for quite a few days, allow them to fail.
2018-11-26Merge PR #9074: Fix ocamldebug-coq for packed gramlibEmilio Jesus Gallego Arias
2018-11-26Fix ocamldebug-coq for packed gramlibGaëtan Gilbert
2018-11-26Put -indices-matter in typing_flagsGaë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-25Merge PR #9036: Add bodies to sphinx objects.Clément Pit-Claudel
2018-11-24[toplevel] Move compilation-related functions to their own module.Emilio Jesus Gallego Arias
We move compilation-specific functions to their own module. This helps isolating `.vo` compile-time functionality from interactive, toplevel-like processing. cc: #8683
2018-11-24[toplevel] Move command line path processing to CoqargsEmilio Jesus Gallego Arias
We move the processing of path-related arguments to `Coqargs`, and following experience from `SerAPI` we stored already-processed `coq_paths` in the `opts` record. This has proven to be very convenient as to avoid duplication of code in the presence of several clients of the `Coqargs` parsing functionality.
2018-11-24Merge PR #8996: Fix #8937: inductive conversion in coqchk subtypingHugo Herbelin
2018-11-24Merge PR #8950: [topfmt] Add phase attribute for toplevel printing.Hugo Herbelin
2018-11-24[checker] Remove duplicated from checker / clibEmilio Jesus Gallego Arias
Now that we link lib we can do this.
2018-11-24Merge PR #8929: Fix fixpoint related lifting in open recursors + related ↵Pierre-Marie Pédrot
cleanups
2018-11-24Merge PR #8933: Make initial evar map argument to check_evars_are_solved ↵Pierre-Marie Pédrot
optional.
2018-11-24Merge PR #9022: [ci] [doc] Split user/developer README, add info about ↵Théo Zimmermann
Nix/Docker CI
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 #8890: Looking for notation both before or after removal of top ↵Emilio Jesus Gallego Arias
coercion
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-23Merge PR #9051: Camlp5 safe API strikes backEmilio Jesus Gallego Arias
2018-11-23Merge PR #8995: Don't redeclare constraints of fields in IncludeMaxime Dénès
2018-11-23Adding overlay.Pierre-Marie Pédrot
2018-11-23Remove the unsafe API from gramlib.Pierre-Marie Pédrot
2018-11-23Remove the unsafe camlp5 API from the Coq codebase.Pierre-Marie Pédrot
2018-11-23Only use Coq API in coqpp.Pierre-Marie Pédrot
2018-11-23Port Pcoq to safe camlp5 API.Pierre-Marie Pédrot
Revival of the cleaning part of #8923.
2018-11-23Merge PR #9021: merge-pr: Improve overlay checkMaxime Dénès
2018-11-23Fix #8937: inductive conversion in coqchk subtypingGaëtan Gilbert
As far as I can tell this is similar to what coqtop does. Delta resolvers are complicated so I may be mistaken. The important part is to avoid losing the modified delta resolver returned by strengthen_and_subst in check_mexpr.
2018-11-22Merge PR #8920: Deprecate Typeclasses Axioms Are InstancesPierre-Marie Pédrot
2018-11-22[dev] fix create_overlay wrt branch names containing /Enrico Tassi
2018-11-22Merge PR #8924: Misc updates to codeownersMaxime Dénès
2018-11-22New code owner team parsing-maintainers.Théo Zimmermann
2018-11-22New code owner team ssreflect-maintainers.Théo Zimmermann
2018-11-22It seems that Hugo is also willing to assume a maintainer role on CoqIDE.Théo Zimmermann
2018-11-22All dune files are owned by dune code owners.Théo Zimmermann
2018-11-22Disable deprecation warnings in compat files.Gaëtan Gilbert
2018-11-22Deprecate Typeclasses Axioms Are InstancesGaëtan Gilbert
People should use Declare Instance instead.
2018-11-22Merge PR #8967: Fix #8922 (uncaught pp_diff exception)Hugo Herbelin
2018-11-22Merge PR #9049: [default.nix] Add graphviz for STM DAG printerVincent Laporte
2018-11-22[default.nix] Add graphviz for STM DAG printerMaxime Dénès
2018-11-21Merge PR #8945: [camlp5] Remove dependency on camlp5.Pierre-Marie Pédrot
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 04:37:13 +0000