index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
Age
Commit message (
Expand
)
Author
2019-12-26
[omega] Remove non-documented "omega with *"
Emilio Jesus Gallego Arias
2019-12-26
Deprecate the "omega with *" syntax.
Pierre-Marie Pédrot
2019-12-25
Show doc notations in boldface
Jim Fehrle
2019-12-24
[Attributes] accept #[canonical] (Let|Definition)
Enrico Tassi
2019-12-24
[CS] Allow a variable introduced with Let to be a canonical instance
Enrico Tassi
2019-12-23
Merge PR #11324: [refman] Mention Ltac2 in intro.
Pierre-Marie Pédrot
2019-12-23
Merge PR #10760: Make rapply handle all numbers of underscores
Pierre-Marie Pédrot
2019-12-22
Apply suggestions from code review
Théo Zimmermann
2019-12-22
[refman] Mention Ltac2 in intro.
Théo Zimmermann
2019-12-22
[refman] Add missing s.
Théo Zimmermann
2019-12-21
Merge PR #11311: Fix handling of recursive notations with custom entries
Hugo Herbelin
2019-12-20
Fix handling of recursive notations with custom entries
Maxime Dénès
2019-12-19
Support additional escape sequences in notations
Jim Fehrle
2019-12-20
Coherence checking for coercions
Kazuhiko Sakaguchi
2019-12-18
Merge PR #11203: Make the string argument of `time` print correctly
Pierre-Marie Pédrot
2019-12-18
Merge PR #11263: [micromega] fix efficiency regression
Maxime Dénès
2019-12-17
Merge PR #10762: Fix refine and eapply to mark shelved goals as non-resolvabl...
Maxime Dénès
2019-12-17
[micromega] fix efficiency regression
Frédéric Besson
2019-12-14
Make prodn look more like productionlist
Jim Fehrle
2019-12-14
Fix refine and eapply to mark shelved goals as non-resolvable, always
Matthieu Sozeau
2019-12-13
[doc] [INSTALL] Port INSTALL to markdown format.
Emilio Jesus Gallego Arias
2019-12-12
restrict minimization to set to flexibles
Gaëtan Gilbert
2019-12-12
Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...
charguer
2019-12-10
Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).
Hugo Herbelin
2019-12-09
Fixes #11254 (not requiring coqlib to be set to report about coqtop version).
Hugo Herbelin
2019-12-06
Make the string argument of `time` print correctly
Jason Gross
2019-12-06
Merge PR #11127: Added theorem Nat.bezout_comm.
Hugo Herbelin
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
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-04
Update doc/changelog/02-specification-language/11233-master+fix11231-missing-...
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
Merge PR #11162: [CS] support #[local] attribute
Maxime Dénès
2019-12-03
Fixes #11231 (missing dependency in pattern-matching decompilation).
Hugo Herbelin
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
List of 8.11 contributors and stats.
Théo Zimmermann
2019-12-02
Merge redundant consecutive changelog entries on reals.
Théo Zimmermann
2019-12-02
Highlight refine attribute for Instance.
Théo Zimmermann
2019-12-02
Warn more clearly about incompatibilities coming from #10476.
Théo Zimmermann
2019-12-02
8.11 release notes.
Matthieu Sozeau
2019-12-02
Move unreleased changelog to new 8.11 section.
Théo Zimmermann
2019-12-02
Merge PR #10575: Clean up deprecations
Théo Zimmermann
2019-12-01
Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.
Gaëtan Gilbert
2019-11-30
Actually deprecate the `cutrewrite` tactic
Maxime Dénès
[prev]
[next]