aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* 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
| | |
* | | Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\ \ \
* | | | Improve documentation of assert / pose proof / specialize.Gravatar Théo Zimmermann2017-05-04
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | This commits documents the as clause of specialize and that the as clause of pose proof is optional. It also mentions a feature of assert ( := ) that was available since 8.5 and was mentionned by @herbelin in: https://github.com/coq/coq/pull/248#issuecomment-297970503
* | | Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
|\ \ \
| | | * Fix outdated description in RefMan.Gravatar Théo Zimmermann2017-05-03
| | | |
* | | | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
| | | |
* | | | Fix for bug 5507. Mispelt de Bruijn.Gravatar Théo Zimmermann2017-05-01
| | | |
* | | | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵Gravatar Maxime Dénès2017-04-28
|\ \ \ \ | | | | | | | | | | | | | | | let-ins
| | | | * fix order of command-line arguments mentioned in Add LoadPathGravatar Paul Steckler2017-04-27
| | | | |
| | | * | Mark transparent_abstract as risky in docsGravatar Jason Gross2017-04-25
| | | | | | | | | | | | | | | | | | | | As per Enrico's request.
| | | * | Add transparent_abstract tacticGravatar Jason Gross2017-04-25
| |_|/ / |/| | |
| | * | refman: remember the old name of template polymorphism.Gravatar Gaetan Gilbert2017-04-24
| | | |
* | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Gravatar Maxime Dénès2017-04-12
|\ \ \ \ | | | | | | | | | | | | | | | record fields.
| | | * | Update RefMan-pre to mention template polymorphism.Gravatar Gaetan Gilbert2017-04-11
| | | | |
| | | * | Use "template polymorphism" in the documentation.Gravatar Gaetan Gilbert2017-04-11
| | | | |
| | | * | Mention template polymorphism in the documentation.Gravatar Gaetan Gilbert2017-04-11
| |_|/ / |/| | | | | | | | | | | Since About mentions it the doc should as well.
* | | | Merge PR#460: Turning the printing primitive projection compatibility flag ↵Gravatar Maxime Dénès2017-04-09
|\ \ \ \ | | | | | | | | | | | | | | | off by default
| | | * | Fixing #5420 as well as many related bugs due to miscounting let-ins.Gravatar Hugo Herbelin2017-04-09
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | - Supporting let-ins in tactic "fix", and hence in interactive Fixpoint and mutual theorems. - Documenting more precisely the meaning of n in tactic "fix id n". - Fixing computation of recursive index at interpretation time in the presence of let-ins.
* | | | Merge PR#485: Document Show MatchGravatar Maxime Dénès2017-04-07
|\ \ \ \
| | * | | Turning the printing primitive projection parameter flag off by default.Gravatar Hugo Herbelin2017-04-07
| | | | |
| | * | | Turning the printing primitive projection compatibility flag off by default.Gravatar Hugo Herbelin2017-04-07
| |/ / / |/| | |
* | | | Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\ \ \ \
| | | * | Documenting the grammar {| ... |} syntax for building records.Gravatar Hugo Herbelin2017-03-23
| |_|/ / |/| | | | | | | | | | | | | | | And an extra minor changes (use of zeroone when relevant, use of type rather than term).
* | | | Merge PR#433: doc: fix a French-ismGravatar Maxime Dénès2017-03-23
|\ \ \ \
* | | | | Fix some typos.Gravatar Guillaume Melquiond2017-03-22
| | | | |
* | | | | Merge PR#482: [toplevel] Remove unusable option -notopGravatar Maxime Dénès2017-03-22
|\ \ \ \ \
| | | | * | Document Show Match, add ref to that in match variants/extensionsGravatar Paul Steckler2017-03-17
| |_|_|/ / |/| | | |
| | * | | doc: fix a French-ismGravatar Valentin Robert2017-03-14
| | | | |
| * | | | [toplevel] Remove unusable option -notopGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Maxime points out that -notop cannot be used as the kernel requires all constants to belong into a module. Indeed: ``` $ rlwrap ./bin/coqtop -notop Coq < Definition foo := True. Toplevel input, characters 0-23: > Definition foo := True. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: No session module started (use -top dir) Coq < Module M. Definition foo := True. End M. Module M is defined Coq < Locate foo. Constant If you see this, it's a bug.M.foo (shorter name to refer to it in current context is M.foo) ``` My rationale for the removal is that this kind of incomplete features are often confusing to newcomers ─ it has happened to me many times ─ as it can be seen for example in #397 .
* | | | | Merge PR#438: Fix V7 syntax in refman.Gravatar Maxime Dénès2017-03-14
|\ \ \ \ \ | |/ / / / |/| | | |
* | | | | Typo doc notations.Gravatar Hugo Herbelin2017-03-09
| | | | |
* | | | | Clarifying doc about interpretation of scopes in notations (#5386).Gravatar Hugo Herbelin2017-03-09
| | | | |
| | | * | Farewell decl_modeGravatar Enrico Tassi2017-03-07
| | |/ / | | | | | | | | | | | | | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
* | | | Adding explicitly a file to work in the context of propositional extensionality.Gravatar Hugo Herbelin2017-03-03
| | | |
* | | | Adding a file providing extensional choice (i.e. choice over setoids).Gravatar Hugo Herbelin2017-03-03
| | | | | | | | | | | | | | | | Also integrating suggestions from Théo.
* | | | Logic library: Adding a characterization of excluded-middle in term ofGravatar Hugo Herbelin2017-03-03
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | choice of a representative in a partition of bool. Also move a result about propositional extensionality from ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by symmetry. Also spotting typos (thanks to Théo).
| * | Fix V7 syntax in refman.Gravatar Théo Zimmermann2017-02-20
|/ /
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\|
| * Fix some typos in tutorial (bug #5294).Gravatar Guillaume Melquiond2016-12-28
| | | | | | | | | | | | This commit uses the proper url for bug reporting, marks urls as such, stops qualifying the Coq'Art book as new, and fix the spacing after the Coq name.
| * Fix incorrect documentation that prevents successful compilation (bug #5265).Gravatar Guillaume Melquiond2016-12-16
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 07:33:40 +0000