aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* 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.
* BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
* 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
| | |
* | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 20:44:01 +0000