index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
/
refman
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.7'
Maxime Dénès
2017-07-20
|
\
|
*
Merge PR #745: Add timing scripts
Maxime Dénès
2017-07-19
|
|
\
*
|
\
Merge PR #865: RefMan-ext: fix some typos
Maxime Dénès
2017-07-17
|
\
\
\
|
*
|
|
Update with non structurally recursive
william-lawvere
2017-07-14
|
|
*
|
Sync the manual with the deprecation warnings.
Théo Zimmermann
2017-07-11
|
|
/
/
|
/
|
|
|
|
*
Document the timing targets
Jason Gross
2017-07-11
|
|
*
Strip trailing spaces
Jason Gross
2017-07-11
|
|
/
|
/
|
|
*
RefMan-ext: fix some typos
William Lawvere
2017-07-07
*
|
Merge PR #835: Remove doc/refman/RefMan-ind.tex
Maxime Dénès
2017-07-07
|
\
\
|
|
/
|
/
|
*
|
Merge PR #837: Add inversion_sigma to CHANGES and to doc
Maxime Dénès
2017-07-05
|
\
\
*
\
\
Merge PR #850: Improve grammar in RefMan-Gal and RefMan-syn
Maxime Dénès
2017-07-05
|
\
\
\
*
\
\
\
Merge PR #832: Document an example `Makefile` for `coq_makefile`
Maxime Dénès
2017-07-05
|
\
\
\
\
*
\
\
\
\
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
|
\
\
\
\
\
|
|
|
*
|
|
Update RefMan-syn.tex
william-lawvere
2017-07-01
|
|
|
*
|
|
Merge remote-tracking branch 'upstream/trunk' into trunk
William Lawvere
2017-07-01
|
|
|
|
\
\
\
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
RefMan-gal: improve grammar
William Lawvere
2017-07-01
|
|
|
*
|
|
RefMan-syn: grammar edit
William Lawvere
2017-07-01
|
|
*
|
|
|
Document an example `Makefile` for `coq_makefile`
Jason Gross
2017-06-30
|
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
Remove doc/refman/RefMan-ind.tex
Jason Gross
2017-06-30
|
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
Add doc for inversion_sigma to RefMan-tac
Jason Gross
2017-06-30
|
|
_
|
/
|
/
|
|
|
*
|
Merge PR#756: Fix Bug #5574, document function scope
Maxime Dénès
2017-06-26
|
|
\
\
|
|
*
|
Fix Bug #5574, document function scope
Paul Steckler
2017-06-23
|
*
|
|
Merge PR#740: Refactor documentation of records.
Maxime Dénès
2017-06-23
|
|
\
\
\
*
|
\
\
\
Merge PR#777: Improving documentation of tactic "move" (report #4561)
Maxime Dénès
2017-06-19
|
\
\
\
\
\
|
|
|
*
|
|
Refactor documentation of records.
Théo Zimmermann
2017-06-16
|
|
|
|
/
/
|
|
*
|
|
Merge PR#767: Document named evars (including Show ident)
Maxime Dénès
2017-06-16
|
|
|
\
\
\
*
|
|
|
|
|
Document cumulativity for inductive types
Amin Timany
2017-06-16
*
|
|
|
|
|
Merge PR#765: Remove obsolete Show commands
Maxime Dénès
2017-06-14
|
\
\
\
\
\
\
*
|
|
|
|
|
|
Prelude : no more autoload of plugins extraction and recdef
Pierre Letouzey
2017-06-14
|
|
|
|
|
|
*
doc: improve grammar of RefMan-syn
William Lawvere
2017-06-13
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
*
|
|
|
Improving documentation of tactic "move" (report #4561).
Hugo Herbelin
2017-06-13
|
|
/
/
/
/
|
/
|
|
|
|
|
|
|
*
|
Document instantiate (ident := term) and make it the preferred variant.
Théo Zimmermann
2017-06-13
|
|
|
*
|
Document Show ident.
Théo Zimmermann
2017-06-13
|
|
|
*
|
Document evar naming syntax.
Théo Zimmermann
2017-06-13
|
|
|
|
/
|
*
|
/
Remove commented documentation for Show Tree.
Théo Zimmermann
2017-06-12
|
/
/
/
|
*
/
Fix documentation of Typeclasses eauto :=
Théo Zimmermann
2017-06-07
|
|
/
*
|
Merge PR#449: make specialize smarter (bug 5370).
Maxime Dénès
2017-06-01
|
\
\
|
*
|
Documenting the new behaviour of specialize.
Pierre Courtieu
2017-05-31
*
|
|
Documentation for eassert, eenough, epose proof, eset, eremember, epose.
Hugo Herbelin
2017-05-30
|
/
/
*
|
Documenting the existence of first and solve as Ltac definitions.
Pierre-Marie Pédrot
2017-05-27
*
|
Merge PR#406: coq makefile2
Maxime Dénès
2017-05-25
|
\
\
|
*
|
add the only target
Enrico Tassi
2017-05-23
|
*
|
enters coq_makefile2
Enrico Tassi
2017-05-23
*
|
|
[vernac] Remove `Save thm id.` command.
Emilio Jesus Gallego Arias
2017-05-23
*
|
|
[vernac] Remove `Save.` command.
Emilio Jesus Gallego Arias
2017-05-23
|
/
/
*
|
Documenting relaxing of constraints on injection.
Hugo Herbelin
2017-05-17
*
|
Merge PR#457: Adding an even more compact goal hyps mode.
Maxime Dénès
2017-05-17
|
\
\
*
\
\
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-05-17
|
\
\
\
|
|
|
/
|
|
/
|
*
|
|
Add documentation for Set Ltac Batch Debug
Jason Gross
2017-05-11
|
|
*
Documenting Printing Compact Contexts + CHANGES
Pierre Courtieu
2017-05-11
[next]