aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
Commit message (Collapse)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
| | | | | | | | | | | | | | | We document the most useful timing targets and variables, how to invoke them, and what the output looks like.
| | * 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
| |/ / / / |/| | | | | | | | | | | | | | | | | | | We document an example `Makefile` which does not include the generated `CoqMakefile`, but instead invokes arbitrary targets in it.
| | | | * Remove doc/refman/RefMan-ind.texGravatar Jason Gross2017-06-30
| |_|_|/ |/| | | | | | | | | | | | | | | It does not seem to be referred to by any file, and does not seem to be built by any implicit rules.
| | | * 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
| | | |/ / | | | | | | | | | | | | | | | This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971
| | * | | 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
| | | | | | * 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
|/ / | | | | | | Includes fixes and suggestions from Théo.
* | 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
| | | | | | | | | | | | | | | | | | | | | | | | This makes the following work correctly: make only TGTS="foo bar" -j2 note that make foo bar -j2 is not doing what you think
| * | enters coq_makefile2Gravatar Enrico Tassi2017-05-23
| | |
* | | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc...
* | | [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
|/ / | | | | | | It has been deprecated for a while in favor of `Qed`.
* | Documenting relaxing of constraints on injection.Gravatar Hugo Herbelin2017-05-17
| | | | | | | | | | We seized this opportunity to do a little refreshing of the section describing injection.
* | 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-29 01:00:23 +0000