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 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
|
|
_
|
/
/
|
/
|
|
|
|
|
|
*
disable async on Windows by default
Paul Steckler
2017-06-26
|
|
_
|
/
|
/
|
|
|
*
|
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
*
|
|
Merge PR#201: Transparent abstract
Maxime Dénès
2017-05-11
|
\
\
\
*
|
|
|
Improve documentation of assert / pose proof / specialize.
Théo Zimmermann
2017-05-04
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR#411: Mention template polymorphism in the documentation.
Maxime Dénès
2017-05-03
|
\
\
\
|
|
|
*
Fix outdated description in RefMan.
Théo Zimmermann
2017-05-03
*
|
|
|
More consistent writing of de Bruijn.
Théo Zimmermann
2017-05-01
*
|
|
|
Fix for bug 5507. Mispelt de Bruijn.
Théo Zimmermann
2017-05-01
*
|
|
|
Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...
Maxime Dénès
2017-04-28
|
\
\
\
\
|
|
|
|
*
fix order of command-line arguments mentioned in Add LoadPath
Paul Steckler
2017-04-27
|
|
|
*
|
Mark transparent_abstract as risky in docs
Jason Gross
2017-04-25
|
|
|
*
|
Add transparent_abstract tactic
Jason Gross
2017-04-25
|
|
_
|
/
/
|
/
|
|
|
|
|
*
|
refman: remember the old name of template polymorphism.
Gaetan Gilbert
2017-04-24
*
|
|
|
Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...
Maxime Dénès
2017-04-12
|
\
\
\
\
|
|
|
*
|
Update RefMan-pre to mention template polymorphism.
Gaetan Gilbert
2017-04-11
[prev]
[next]