aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-09-29Replacing Refine.pr_constr by Termops.Internal.print_constr.Hugo Herbelin
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-28Cleanup comparisons in econstr (compare_head_... users)Gaëtan Gilbert
2018-09-28Generalize type of compare_head_with functionsGaëtan Gilbert
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-28Small fixes in attribute documentation.Théo Zimmermann
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-27[dune] [merlin] Fix some usability issues.Emilio 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-27Unification failure: don't give preference to a "beyond capabilities" error.Hugo Herbelin
2018-09-27Preparing ability to select "best" unification failure to report among two.Hugo Herbelin
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-27Remove {Safe_typing,Global}.push_contextGaëtan Gilbert
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-27Overlays for Ltac2 and Equations.Hugo Herbelin
2018-09-27Fixes #8553 (regression of tactic "change" under binders).Hugo Herbelin
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[ocaml] Update required OCaml version to 4.05.0Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 19:48:09 +0000