index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-08-28
Adding overlay for coq-elpi.
Hugo Herbelin
2020-08-28
About: Add a mention that arguments have been renamed, if ever it is the case.
Hugo Herbelin
2020-08-28
Where there are several lists of implicit arguments, don't pretend names matter.
Hugo Herbelin
2020-08-28
Do not write "rename" for arguments in About, since these arguments are valid...
Hugo Herbelin
2020-08-28
When printing the type in About, use the renamed arguments.
Hugo Herbelin
2020-08-28
When reporting an implicit argument error on a rename argument, use the renam...
Hugo Herbelin
2020-08-28
In "About", print all arguments, even if it is trailing list of _.
Hugo Herbelin
2020-08-28
Add test for past anomaly
Gaëtan Gilbert
2020-08-28
par: print relevant subgoal when failing
Gaëtan Gilbert
2020-08-28
Proof using cleanup, small doc addition and fix using Type in collections
Gaëtan Gilbert
2020-08-28
Merge PR #12924: Remove meta-based refiner code in ssr
coqbot-app[bot]
2020-08-28
Merge PR #12632: [state] A few nits after consolidation of state.
coqbot-app[bot]
2020-08-27
[zarith] Changelog
Emilio Jesus Gallego Arias
2020-08-27
[nsatz] num → zarith
Vincent Laporte
2020-08-27
[numtok] [zarith] Simplifications
Emilio Jesus Gallego Arias
2020-08-27
[zarith] [notation] Build less intermediate values
Emilio Jesus Gallego Arias
2020-08-27
[numeral] [plugins] Switch from `Big_int` to ZArith.
Emilio Jesus Gallego Arias
2020-08-27
[state] A few nits after consolidation of state.
Emilio Jesus Gallego Arias
2020-08-27
Remove the now unused Evarutil.mk_new_meta function.
Pierre-Marie Pédrot
2020-08-27
Remove a call to the old refiner in ssr.
Pierre-Marie Pédrot
2020-08-27
Merge PR #12922: Fix .gitignore after the merge of #12849.
coqbot-app[bot]
2020-08-27
Fix .gitignore after the merge of #12849.
Pierre-Marie Pédrot
2020-08-27
Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfoo
Pierre-Marie Pédrot
2020-08-27
Merge PR #12862: [coqchk] Look inside inner modules as well
Pierre-Marie Pédrot
2020-08-27
Merge PR #12918: tacinterp mini cleanup useless letin
Pierre-Marie Pédrot
2020-08-27
Merge PR #12499: Clean future goals
Pierre-Marie Pédrot
2020-08-27
Merge PR #12913: Modify lia to work with -mangle-names
coqbot-app[bot]
2020-08-27
Merge PR #12850: Avoid running configure when plugins/ modified
coqbot-app[bot]
2020-08-27
Merge PR #12877: Propagate in-context information for explicitation of extra ...
coqbot-app[bot]
2020-08-27
Merge PR #12867: Fast freeze summary
coqbot-app[bot]
2020-08-27
Merge PR #12911: Use the lite variants of performance tests in the bench defa...
coqbot-app[bot]
2020-08-27
tacinterp mini cleanup useless letin
Gaëtan Gilbert
2020-08-27
Merge PR #12898: [ssr] backport ssrbool from Math Comp 1.11
Enrico Tassi
2020-08-26
Merge PR #12085: Convert ltac2 chapter to use prodn, update syntax
coqbot-app[bot]
2020-08-26
Modify lia to work with -mangle-names
Jasper Hugunin
2020-08-26
Wrap future goals into a module
Maxime Dénès
2020-08-26
Add test for #10939
Maxime Dénès
2020-08-26
Make future_goals stack explicit in the evarmap
Maxime Dénès
2020-08-26
Move given_up goals to evar_map
Maxime Dénès
2020-08-26
Better encapsulation of future goals
Maxime Dénès
2020-08-26
Fix algebraic comparison with sprop on one side
Gaëtan Gilbert
2020-08-26
Use the lite variants of performance tests in the bench default packages.
Pierre-Marie Pédrot
2020-08-26
Merge PR #12764: A fix and two enhancements of trailing pattern factorization...
Pierre-Marie Pédrot
2020-08-26
Merge PR #12904: Move bench job definition to its own file
Pierre-Marie Pédrot
2020-08-26
Merge PR #12881: Deprecate intro_using
Pierre-Marie Pédrot
2020-08-26
Merge PR #12901: [bench] Remove useless commit guessing logic
Pierre-Marie Pédrot
2020-08-26
Merge PR #12884: Documentation of coq_makefile: fix name of installation dir ...
coqbot-app[bot]
2020-08-26
Merge PR #12861: Require NsatzTactic: nsatz support for Z and Q
Pierre-Marie Pédrot
2020-08-26
address comments and fixups
Reynald Affeldt
2020-08-25
Documentation of coq_makefile: fix name of installation dir + help on option -f.
Hugo Herbelin
[prev]
[next]