index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
Commit message (
Expand
)
Author
Age
*
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
|
|
/
/
/
|
/
|
|
|
|
|
|
*
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#375: Deprecation
Maxime Dénès
2017-06-15
|
\
\
\
\
\
\
*
\
\
\
\
\
\
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
|
|
|
|
|
|
|
*
Merge remote-tracking branch 'upstream/trunk' into trunk
William Lawvere
2017-06-13
|
|
|
|
|
|
|
|
\
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
Remove support for Coq 8.4.
Guillaume Melquiond
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
|
|
|
|
_
|
_
|
/
|
|
|
/
|
|
|
*
|
/
|
|
|
BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)
Pierre Letouzey
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
[next]