index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
sphinx
Age
Commit message (
Expand
)
Author
2019-11-01
docs(gallina-extensions.rst): Say more on float literals extraction
Erik Martin-Dorel
2019-11-01
docs: Add refman+stdlib documentation
Erik Martin-Dorel
2019-10-31
Merge PR #10985: Print argument info as an Arguments command in About
Emilio Jesus Gallego Arias
2019-10-31
Merge PR #9883: Add support for Sorts in numeral notations
Vincent Laporte
2019-10-31
Merge PR #10997: Implement the unsupported attribute error using the warning ...
Emilio Jesus Gallego Arias
2019-10-31
Doc: index command Arguments with assert
Gaëtan Gilbert
2019-10-31
Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.
Gaëtan Gilbert
2019-10-30
Implement the unsupported attribute error using the warning system
Gaëtan Gilbert
2019-10-30
Use bullets and indentation (but the result rendering is weird).
Théo Zimmermann
2019-10-30
Use explicit match as suggested by Clément.
Théo Zimmermann
2019-10-30
[refman] Add a second example of contradiction when positivity checking is di...
Théo Zimmermann
2019-10-30
[refman] Give an example of contradiction when positivity checking is disabled.
Théo Zimmermann
2019-10-30
Merge PR #10494: Show diffs in "Show Proof."
Enrico Tassi
2019-10-29
Show diffs in "Show Proof."
Jim Fehrle
2019-10-29
Fix #9114, assert_succeeds (exact I) solves goal
Jason Gross
2019-10-29
`assert_succeeds`&`assert_fails`: multisuccess fix
Jason Gross
2019-10-29
Document the ability to bind notation arguments in Ltac2.
Pierre-Marie Pédrot
2019-10-28
Add support for Sorts in numeral notations
Jason Gross
2019-10-24
Release notes for Coq 8.10.1
Vincent Laporte
2019-10-23
Better wording for "Show Proof" and fix typos
Jim Fehrle
2019-10-23
Merge PR #10929: documentation fixes
Théo Zimmermann
2019-10-22
documentation fixes
Antonio Nikishaev
2019-10-22
Merge PR #10880: Allow to pass Ltac1 values to Ltac2 quotations.
Jason Gross
2019-10-18
Allow to pass Ltac1 values to Ltac2 quotations.
Pierre-Marie Pédrot
2019-10-16
Define sphinx replacements for \SProp \Type etc
Gaëtan Gilbert
2019-10-15
Merge PR #10854: Fix alphabetical ordering in contributors to 8.10.0.
Clément Pit-Claudel
2019-10-14
Merge PR #10883: Doc update with mlg extension - fix #10855
Jason Gross
2019-10-14
Merge PR #10811: Allow SProp default on
Pierre-Marie Pédrot
2019-10-13
Doc update with mlg extension - fix #10855
mcaci
2019-10-11
Merge PR #10489: Fix output for "Printing Dependent Evars Line"
Hugo Herbelin
2019-10-09
Fix alphabetical ordering in the list of contributors to 8.10.
Théo Zimmermann
2019-10-06
Merge PR #10834: Fix #10831: minor issues in documentation of Function.
Clément Pit-Claudel
2019-10-06
Fix #10831: minor issues in documentation of Function.
Théo Zimmermann
2019-10-06
8.10.0 release notes.
Théo Zimmermann
2019-10-05
Merge PR #10763: Fix syntax of reduction tactics when listing qualid to reduc...
Vincent Laporte
2019-10-04
Improve language.
Théo Zimmermann
2019-10-04
Merge PR #9772: [Stdlib] OrderedType: do not pollute the “core” hint data...
Pierre-Marie Pédrot
2019-10-04
Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ...
Pierre-Marie Pédrot
2019-10-04
Allow SProp default on
Gaëtan Gilbert
2019-10-04
[Stdlib] OrderedType: do not pollute the “core” hint database
Vincent Laporte
2019-10-03
Improved handling of micromega caches
Frédéric Besson
2019-10-02
Loosen restrictions on mixing universe mono/polymorphism in sections
Gaëtan Gilbert
2019-09-25
Adding documentation for the move of sections data to kernel.
Pierre-Marie Pédrot
2019-09-19
Fix #10420 Add dependent evar mapping info to output
Jim Fehrle
2019-09-18
Fix syntax of reduction tactics when listing qualid to reduce or not.
Théo Zimmermann
2019-09-16
Re-implementation of zify
Frédéric Besson
2019-09-12
Merge PR #10753: Release notes for 8.10+beta3.
Clément Pit-Claudel
2019-09-12
Release notes for 8.10+beta3.
Théo Zimmermann
2019-09-10
Refman: To be compatible gtk2/gtk3, not mentioning GTK+ version explicitely.
Hugo Herbelin
2019-09-10
Fixing coqide doc about location of "coqiderc" and "coqide.bindings".
Hugo Herbelin
[next]