index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-12-11
Remove the unused add_leaves Libobject primitive.
Pierre-Marie Pédrot
2019-12-11
Remove the reliance of ring objects on the named part.
Pierre-Marie Pédrot
2019-12-11
Merge PR #11262: [hashset] Don't use deprecated Obj.truncate
Pierre-Marie Pédrot
2019-12-11
Merge PR #11271: Fixing #9893. "Specialize with" would not support hyps type ...
Pierre-Marie Pédrot
2019-12-10
Merge PR #10202: Slightly more robust manual implicit arguments
Emilio Jesus Gallego Arias
2019-12-10
Merge PR #11269: Several cleanups and factorization in scheme declarations
Emilio Jesus Gallego Arias
2019-12-10
Fixing #9893 (Letins not supported in the specialized hypothesis).
Pierre Courtieu
2019-12-10
Side-effect free wrapper around already declared schemes.
Pierre-Marie Pédrot
2019-12-10
Make explicit that users should not observe return values of scheme functions.
Pierre-Marie Pédrot
2019-12-10
Simplify internal flags in scheme declarations.
Pierre-Marie Pédrot
2019-12-10
Merge PR #11268: dune: Add byte mode for coqchk and coqide (fix dune-dbg for ...
Emilio Jesus Gallego Arias
2019-12-09
dune: Add byte mode for coqchk and coqide (fix dune-dbg for dune 2)
Gaëtan Gilbert
2019-12-09
Merge PR #11255: Fix #11254: "coqtop --version" working even in the middle of...
Emilio Jesus Gallego Arias
2019-12-09
Fixes #11254 (not requiring coqlib to be set to report about coqtop version).
Hugo Herbelin
2019-12-09
Merge PR #10829: Section.t is never empty
Pierre-Marie Pédrot
2019-12-09
Merge PR #11234: [ide] Don't use -linkall for the GUI app.
Pierre-Marie Pédrot
2019-12-09
[hashset] Don't use deprecated Obj.truncate
Emilio Jesus Gallego Arias
2019-12-09
Merge PR #11256: [configure] [dune] Fix configure under Dune in 32bit builds.
Théo Zimmermann
2019-12-07
Section.t is never empty
Gaëtan Gilbert
2019-12-07
[configure] [dune] Fix configure under Dune in 32bit builds.
Emilio Jesus Gallego Arias
2019-12-07
Merge PR #11141: Moving the diversity of constr printers to a label style
Emilio Jesus Gallego Arias
2019-12-06
Adding documentation in printer.mli
Hugo Herbelin
2019-12-06
Adding overlay for Quickchick PR#145.
Hugo Herbelin
2019-12-06
Moving the diversity of constr printers to a label style.
Hugo Herbelin
2019-12-06
Merge PR #11127: Added theorem Nat.bezout_comm.
Hugo Herbelin
2019-12-06
Merge PR #11232: Remove latex files that should be regenerated by make
Théo Zimmermann
2019-12-06
Merge PR #11174: [dune] Update to dune language version 2.0
Théo Zimmermann
2019-12-05
Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntax
Emilio Jesus Gallego Arias
2019-12-05
Merge PR #11172: Interleave removal of coercions and search for notations
Emilio Jesus Gallego Arias
2019-12-05
Unfortunate bug with "cofix with": case of a CProdN over no bindings.
Hugo Herbelin
2019-12-05
Added Nat.bezout_comm.
Daniel de Rauglaudre
2019-12-05
Merge PR #11210: Tacinterp: push_trace doesn't need to be wrapped in a tactic
Pierre-Marie Pédrot
2019-12-04
Manual implicit arguments: more robustness tests.
Hugo Herbelin
2019-12-04
Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident.
Hugo Herbelin
2019-12-04
Overlay for ELPI
Hugo Herbelin
2019-12-04
[dune] Update to dune language version 2.0
Emilio Jesus Gallego Arias
2019-12-03
Update doc/changelog/03-notations/11172-master+coercion-notation-interleaved-...
Hugo Herbelin
2019-12-03
Printing: Interleaving search for notations and removal of coercions.
Hugo Herbelin
2019-12-03
Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.
Emilio Jesus Gallego Arias
2019-12-03
[ide] Don't use -linkall for the GUI app.
Emilio Jesus Gallego Arias
2019-12-03
Merge PR #11162: [CS] support #[local] attribute
Maxime Dénès
2019-12-03
Merge PR #11175: coercion functions are never called without a term to coerce
Enrico Tassi
2019-12-02
Remove latex files that should be regenerated by make
Jim Fehrle
2019-12-02
Merge PR #11198: Display more information when complexity tests fail
Hugo Herbelin
2019-12-02
Merge PR #11227: Allow to override build date with SOURCE_DATE_EPOCH
Emilio Jesus Gallego Arias
2019-12-02
Remove deprecated compat modifier of Notation / Infix commands.
Théo Zimmermann
2019-12-02
Allow to override build date with SOURCE_DATE_EPOCH
Bernhard M. Wiedemann
2019-12-02
[CS] support #[local] attribute
Enrico Tassi
2019-12-02
Merge PR #11165: [CI] Test latest artifacts of SF instead of the stable version
Emilio Jesus Gallego Arias
2019-12-02
[ci] [sf] Add authentication to artifact download.
Emilio Jesus Gallego Arias
[next]