index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2018-10-01
[dune] [configure] Fix typo in default prefix setting.
Emilio Jesus Gallego Arias
2018-09-30
Merge PR #8599: Typo in top_printers.ml
Pierre-Marie Pédrot
2018-09-30
Merge PR #8590: Functionalizing calls to the environment in Himsg
Pierre-Marie Pédrot
2018-09-30
Merge PR #8597: [dune] Enable warning 60 [unused local module]
Théo Zimmermann
2018-09-30
Typo in top_printers.ml.
Hugo Herbelin
2018-09-29
[dune] Enable warning 60 [unused local module]
Emilio Jesus Gallego Arias
2018-09-29
Merge PR #8588: [dune] Pack checker to avoid [odoc] problems + build doc for ...
Théo Zimmermann
2018-09-28
Functionalizing 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-28
Merge PR #262: A cleaning step in using heuristics for inference of the retur...
Pierre-Marie Pédrot
2018-09-28
Merge PR #8578: [dune] Allow to build CI after a Dune build.
Gaëtan Gilbert
2018-09-28
Merge PR #8479: Fix #8478: Undeclared universe anomaly with sections
Pierre-Marie Pédrot
2018-09-28
Merge PR #8509: Fix numerous anomalies with Scheme Equality
Pierre-Marie Pédrot
2018-09-28
Merge PR #8576: [api] Remove unnecessary type alias introduced in 8.9
Pierre-Marie Pédrot
2018-09-28
Merge PR #8569: [dune] [configure] Further tweaks for interactive use.
Théo Zimmermann
2018-09-28
Merge PR #8568: [dune] [coqide] Turn CoqIDE into a library.
Théo Zimmermann
2018-09-27
A word about PR #262 in CHANGES.
Hugo Herbelin
2018-09-27
Possible abstractions over goal variables when inferring match return clause.
Hugo Herbelin
2018-09-27
Trying an abstracting dependencies heuristic for the match return clause even...
Hugo Herbelin
2018-09-27
Trying a no-inversion no-dependency heuristic for match return clause.
Hugo Herbelin
2018-09-27
Inference of return clause: giving uniformly priority to "small inversion".
Hugo Herbelin
2018-09-27
Merge PR #8545: Functionalize evarmap passing in Cases.ml
Emilio Jesus Gallego Arias
2018-09-27
Merge PR #8570: [ssr] [camlp5] Remove warning from camlp5
Enrico 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 lib
Emilio Jesus Gallego Arias
2018-09-27
[api] Remove unnecessary type alias introduced in 8.9
Emilio Jesus Gallego Arias
2018-09-27
Merge PR #6524: [print] Restrict use of "debug" Termops printer.
Pierre-Marie Pédrot
2018-09-27
Merge PR #8559: [api] Two more missing deprecations.
Pierre-Marie Pédrot
2018-09-27
Using Constant.change_label (better level of abstraction to build kernel names).
Hugo Herbelin
2018-09-27
Scheme Equality: support for working in a context of Parameters.
Hugo Herbelin
2018-09-27
Fixing a Scheme Equality anomaly with constants bound to inductive.
Hugo Herbelin
2018-09-27
Fixing a typo in a comment.
Hugo Herbelin
2018-09-27
Fixing #4859 (anomaly with Scheme called on inductive type with indices).
Hugo Herbelin
2018-09-27
Fixing #4612 (anomaly with Scheme called on unsupported inductive type).
Hugo Herbelin
2018-09-27
Fix #8478: Undeclared universe anomaly with sections
Gaëtan Gilbert
2018-09-27
Merge PR #8475: Centralize the reliance on abstract universe context internals
Gaëtan Gilbert
2018-09-27
Merge PR #8562: [build] Re-enable warning 59.
Gaëtan Gilbert
2018-09-27
Merge PR #8571: [stdlib] Fix warning due to missing Declare Scope in Bvector
Hugo Herbelin
2018-09-27
[stdlib] Fix warning due to missing Declare Scope in Bvector
Emilio Jesus Gallego Arias
2018-09-27
[ssr] [camlp5] Remove warning from camlp5
Emilio Jesus Gallego Arias
2018-09-27
[dune] [coqide] Turn CoqIDE into a library.
Emilio Jesus Gallego Arias
2018-09-26
Merge PR #8171: Bvector: add BVeq and some notations
Hugo 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-26
Merge PR #8561: Fix votour compilation after #8102.
Emilio Jesus Gallego Arias
2018-09-26
Fix votour compilation after #8102.
Pierre-Marie Pédrot
2018-09-26
Merge PR #8102: Fix #8043: Unsafe assignment in checker.
Maxime Dénès
2018-09-26
Merge PR #8497: Use "rm -rf" in "make clean" so .coq-native directories are r...
Maxime Dénès
[next]