aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
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
2018-09-26Inline the definition of CClosure.mk_clos_deep.Pierre-Marie Pédrot
2018-09-26Merge PR #8504: Allow successive attributes #[foo] #[bar]Vincent Laporte
2018-09-26Merge PR #8506: [ssr] use the right environment in ssrpattern (fix #8454)Maxime Dénès
2018-09-26Merge PR #8534: Checking if low-level name printers are used on purpose or notMaxime Dénès
2018-09-26Merge PR #7571: [kernel] Compile with almost all warnings enabled.Maxime Dénès
2018-09-26Make the warning for non-imported hints compatible with internal backtracking.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 14:42:25 +0000