aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-26Merge PR #9063: [checker] Remove duplicated code from checker / clibPierre-Marie Pédrot
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-25Merge PR #9036: Add bodies to sphinx objects.Clément Pit-Claudel
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.
2018-11-21Merge PR #9005: More informative error on vo validation failurePierre-Marie Pédrot
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-21Merge PR #8975: Minor update to micromega.rstThéo Zimmermann
2018-11-21More informative error on vo validation failureGaëtan Gilbert
Now that the checker shares code with the kernel using md5 cic.mli doesn't work. We could md5 declarations.ml but this would miss changes to constr (and cic.mli already missed changes to names, univs). Instead we just print a bit of information (the last seen type name/annotation) when validate fails. This should help debugging when forgetting to update values.ml without the full verbosity of -debug. As such there is no need to -debug in the makefile validate target (NB: CI has an independent implementation of the validate rule since the vos are installed there).
2018-11-21Add overlay for solve-remaining-evars-initial-argGaëtan Gilbert
2018-11-21Make initial evar map argument to check_evars_are_solved optional.Gaëtan Gilbert
(same for solve_remaining_evars) This is the standard way to use these functions, with 1 exception in Unification.
2018-11-21Merge PR #8961: dune: link kernel in checker instead of copying filesPierre-Marie Pédrot
2018-11-21Merge PR #8998: [legacy proof engine] Remove some cruft.Pierre-Marie Pédrot
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 11:27:46 +0000