aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
Commit message (Expand)AuthorAge
* Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\
| * Merge PR #745: Add timing scriptsGravatar Maxime Dénès2017-07-19
| |\
* | \ Merge PR #865: RefMan-ext: fix some typosGravatar Maxime Dénès2017-07-17
|\ \ \
| * | | Update with non structurally recursiveGravatar william-lawvere2017-07-14
| | * | Sync the manual with the deprecation warnings.Gravatar Théo Zimmermann2017-07-11
| |/ / |/| |
| | * Document the timing targetsGravatar Jason Gross2017-07-11
| | * Strip trailing spacesGravatar Jason Gross2017-07-11
| |/ |/|
| * RefMan-ext: fix some typosGravatar William Lawvere2017-07-07
* | Merge PR #835: Remove doc/refman/RefMan-ind.texGravatar Maxime Dénès2017-07-07
|\ \ | |/ |/|
* | Merge PR #837: Add inversion_sigma to CHANGES and to docGravatar Maxime Dénès2017-07-05
|\ \
* \ \ Merge PR #850: Improve grammar in RefMan-Gal and RefMan-synGravatar Maxime Dénès2017-07-05
|\ \ \
* \ \ \ Merge PR #832: Document an example `Makefile` for `coq_makefile`Gravatar Maxime Dénès2017-07-05
|\ \ \ \
* \ \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \ \ \ \
| | | * | | Update RefMan-syn.texGravatar william-lawvere2017-07-01
| | | * | | Merge remote-tracking branch 'upstream/trunk' into trunkGravatar William Lawvere2017-07-01
| | | |\ \ \ | |_|_|/ / / |/| | | | |
| | | * | | RefMan-gal: improve grammarGravatar William Lawvere2017-07-01
| | | * | | RefMan-syn: grammar editGravatar William Lawvere2017-07-01
| | * | | | Document an example `Makefile` for `coq_makefile`Gravatar Jason Gross2017-06-30
| |/ / / / |/| | | |
| | | | * Remove doc/refman/RefMan-ind.texGravatar Jason Gross2017-06-30
| |_|_|/ |/| | |
| | | * Add doc for inversion_sigma to RefMan-tacGravatar Jason Gross2017-06-30
| |_|/ |/| |
| * | Merge PR#756: Fix Bug #5574, document function scopeGravatar Maxime Dénès2017-06-26
| |\ \
| | * | Fix Bug #5574, document function scopeGravatar Paul Steckler2017-06-23
| * | | Merge PR#740: Refactor documentation of records.Gravatar Maxime Dénès2017-06-23
| |\ \ \
* | \ \ \ Merge PR#777: Improving documentation of tactic "move" (report #4561)Gravatar Maxime Dénès2017-06-19
|\ \ \ \ \
| | | * | | Refactor documentation of records.Gravatar Théo Zimmermann2017-06-16
| | | |/ /
| | * | | Merge PR#767: Document named evars (including Show ident)Gravatar Maxime Dénès2017-06-16
| | |\ \ \
* | | | | | Document cumulativity for inductive typesGravatar Amin Timany2017-06-16
* | | | | | Merge PR#765: Remove obsolete Show commandsGravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \
* | | | | | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | * doc: improve grammar of RefMan-synGravatar William Lawvere2017-06-13
| |_|_|_|_|/ |/| | | | |
| | * | | | Improving documentation of tactic "move" (report #4561).Gravatar Hugo Herbelin2017-06-13
| |/ / / / |/| | | |
| | | * | Document instantiate (ident := term) and make it the preferred variant.Gravatar Théo Zimmermann2017-06-13
| | | * | Document Show ident.Gravatar Théo Zimmermann2017-06-13
| | | * | Document evar naming syntax.Gravatar Théo Zimmermann2017-06-13
| | | |/
| * | / Remove commented documentation for Show Tree.Gravatar Théo Zimmermann2017-06-12
|/ / /
| * / Fix documentation of Typeclasses eauto :=Gravatar Théo Zimmermann2017-06-07
| |/
* | Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\ \
| * | Documenting the new behaviour of specialize.Gravatar Pierre Courtieu2017-05-31
* | | Documentation for eassert, eenough, epose proof, eset, eremember, epose.Gravatar Hugo Herbelin2017-05-30
|/ /
* | Documenting the existence of first and solve as Ltac definitions.Gravatar Pierre-Marie Pédrot2017-05-27
* | Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \
| * | add the only targetGravatar Enrico Tassi2017-05-23
| * | enters coq_makefile2Gravatar Enrico Tassi2017-05-23
* | | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
* | | [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
|/ /
* | Documenting relaxing of constraints on injection.Gravatar Hugo Herbelin2017-05-17
* | Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\ \
* \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
|\ \ \ | | |/ | |/|
* | | Add documentation for Set Ltac Batch DebugGravatar Jason Gross2017-05-11
| | * Documenting Printing Compact Contexts + CHANGESGravatar Pierre Courtieu2017-05-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 05:22:03 +0000