aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-10-01[dune] [configure] Fix typo in default prefix setting.Emilio Jesus Gallego Arias
2018-09-30Merge PR #8599: Typo in top_printers.mlPierre-Marie Pédrot
2018-09-30Merge PR #8590: Functionalizing calls to the environment in HimsgPierre-Marie Pédrot
2018-09-30 Merge PR #8597: [dune] Enable warning 60 [unused local module]Théo Zimmermann
2018-09-30Typo in top_printers.ml.Hugo Herbelin
2018-09-29[dune] Enable warning 60 [unused local module]Emilio Jesus Gallego Arias
2018-09-29Merge PR #8588: [dune] Pack checker to avoid [odoc] problems + build doc for ...Théo Zimmermann
2018-09-28Functionalizing calls to the environment in Himsg.Hugo Herbelin
2018-09-28[dune] Pack checker to avoid [odoc] problems + build doc for plugins.Emilio Jesus Gallego Arias
2018-09-28Merge PR #262: A cleaning step in using heuristics for inference of the retur...Pierre-Marie Pédrot
2018-09-28Merge PR #8578: [dune] Allow to build CI after a Dune build.Gaëtan Gilbert
2018-09-28Merge PR #8479: Fix #8478: Undeclared universe anomaly with sectionsPierre-Marie Pédrot
2018-09-28Merge PR #8509: Fix numerous anomalies with Scheme EqualityPierre-Marie Pédrot
2018-09-28Merge PR #8576: [api] Remove unnecessary type alias introduced in 8.9Pierre-Marie Pédrot
2018-09-28Merge PR #8569: [dune] [configure] Further tweaks for interactive use.Théo Zimmermann
2018-09-28Merge PR #8568: [dune] [coqide] Turn CoqIDE into a library.Théo Zimmermann
2018-09-27A word about PR #262 in CHANGES.Hugo Herbelin
2018-09-27Possible abstractions over goal variables when inferring match return clause.Hugo Herbelin
2018-09-27Trying an abstracting dependencies heuristic for the match return clause even...Hugo Herbelin
2018-09-27Trying a no-inversion no-dependency heuristic for match return clause.Hugo Herbelin
2018-09-27Inference of return clause: giving uniformly priority to "small inversion".Hugo Herbelin
2018-09-27Merge PR #8545: Functionalize evarmap passing in Cases.mlEmilio Jesus Gallego Arias
2018-09-27Merge PR #8570: [ssr] [camlp5] Remove warning from camlp5Enrico Tassi
2018-09-27[configure] [dune] Don't force the Dune user to set envars.Emilio Jesus Gallego Arias
2018-09-27[configure] Don't die if the build sandbox doesn't have the stdlib.Emilio Jesus Gallego Arias
2018-09-27[ci] Allow `make ci-$contrib` when we have a build under Dune.Emilio Jesus Gallego Arias
2018-09-27[coqc] Use standard binary location routine from libEmilio Jesus Gallego Arias
2018-09-27[api] Remove unnecessary type alias introduced in 8.9Emilio Jesus Gallego Arias
2018-09-27Merge PR #6524: [print] Restrict use of "debug" Termops printer.Pierre-Marie Pédrot
2018-09-27Merge PR #8559: [api] Two more missing deprecations.Pierre-Marie Pédrot
2018-09-27Using Constant.change_label (better level of abstraction to build kernel names).Hugo Herbelin
2018-09-27Scheme Equality: support for working in a context of Parameters.Hugo Herbelin
2018-09-27Fixing a Scheme Equality anomaly with constants bound to inductive.Hugo Herbelin
2018-09-27Fixing a typo in a comment.Hugo Herbelin
2018-09-27Fixing #4859 (anomaly with Scheme called on inductive type with indices).Hugo Herbelin
2018-09-27Fixing #4612 (anomaly with Scheme called on unsupported inductive type).Hugo Herbelin
2018-09-27Fix #8478: Undeclared universe anomaly with sectionsGaëtan Gilbert
2018-09-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-27Merge PR #8562: [build] Re-enable warning 59.Gaëtan Gilbert
2018-09-27Merge PR #8571: [stdlib] Fix warning due to missing Declare Scope in BvectorHugo Herbelin
2018-09-27[stdlib] Fix warning due to missing Declare Scope in BvectorEmilio Jesus Gallego Arias
2018-09-27[ssr] [camlp5] Remove warning from camlp5Emilio Jesus Gallego Arias
2018-09-27[dune] [coqide] Turn CoqIDE into a library.Emilio Jesus Gallego Arias
2018-09-26Merge PR #8171: Bvector: add BVeq and some notationsHugo Herbelin
2018-09-26[build] Re-enable warning 59.Emilio Jesus Gallego Arias
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-09-26Merge PR #8561: Fix votour compilation after #8102.Emilio Jesus Gallego Arias
2018-09-26Fix votour compilation after #8102.Pierre-Marie Pédrot
2018-09-26Merge PR #8102: Fix #8043: Unsafe assignment in checker.Maxime Dénès
2018-09-26Merge PR #8497: Use "rm -rf" in "make clean" so .coq-native directories are r...Maxime Dénès