Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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 |
| | | | | | | | | | | | | | | | | 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_makefile2 | Enrico Tassi | 2017-05-23 |
| | | |||
* | | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias | 2017-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. | Emilio Jesus Gallego Arias | 2017-05-23 |
|/ | | | | It has been deprecated for a while in favor of `Qed`. | ||
* | Documenting relaxing of constraints on injection. | Hugo Herbelin | 2017-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. | 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 |
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | 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. | 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 |
| | | | | |||
* | | | | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵ | Maxime Dénès | 2017-04-28 |
|\ \ \ \ | | | | | | | | | | | | | | | | let-ins | ||
| | | | * | fix order of command-line arguments mentioned in Add LoadPath | Paul Steckler | 2017-04-27 |
| | | | | | |||
| | | * | | Mark transparent_abstract as risky in docs | Jason Gross | 2017-04-25 |
| | | | | | | | | | | | | | | | | | | | | As per Enrico's request. | ||
| | | * | | Add transparent_abstract tactic | Jason Gross | 2017-04-25 |
| |_|/ / |/| | | | |||
| | * | | refman: remember the old name of template polymorphism. | Gaetan Gilbert | 2017-04-24 |
| | | | | |||
* | | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵ | Maxime Dénès | 2017-04-12 |
|\ \ \ \ | | | | | | | | | | | | | | | | record fields. | ||
| | | * | | Update RefMan-pre to mention template polymorphism. | Gaetan Gilbert | 2017-04-11 |
| | | | | | |||
| | | * | | Use "template polymorphism" in the documentation. | Gaetan Gilbert | 2017-04-11 |
| | | | | | |||
| | | * | | Mention template polymorphism in the documentation. | Gaetan Gilbert | 2017-04-11 |
| |_|/ / |/| | | | | | | | | | | | Since About mentions it the doc should as well. | ||
* | | | | Merge PR#460: Turning the printing primitive projection compatibility flag ↵ | Maxime Dénès | 2017-04-09 |
|\ \ \ \ | | | | | | | | | | | | | | | | off by default | ||
| | | * | | Fixing #5420 as well as many related bugs due to miscounting let-ins. | Hugo Herbelin | 2017-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 Match | Maxime Dénès | 2017-04-07 |
|\ \ \ \ | |||
| | * | | | Turning the printing primitive projection parameter flag off by default. | Hugo Herbelin | 2017-04-07 |
| | | | | | |||
| | * | | | Turning the printing primitive projection compatibility flag off by default. | Hugo Herbelin | 2017-04-07 |
| |/ / / |/| | | | |||
* | | | | Merge PR#455: Farewell decl_mode | Maxime Dénès | 2017-04-06 |
|\ \ \ \ | |||
| | | * | | Documenting the grammar {| ... |} syntax for building records. | Hugo Herbelin | 2017-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-ism | Maxime Dénès | 2017-03-23 |
|\ \ \ \ | |||
* | | | | | Fix some typos. | Guillaume Melquiond | 2017-03-22 |
| | | | | | |||
* | | | | | Merge PR#482: [toplevel] Remove unusable option -notop | Maxime Dénès | 2017-03-22 |
|\ \ \ \ \ | |||
| | | | * | | Document Show Match, add ref to that in match variants/extensions | Paul Steckler | 2017-03-17 |
| |_|_|/ / |/| | | | | |||
| | * | | | doc: fix a French-ism | Valentin Robert | 2017-03-14 |
| | | | | | |||
| * | | | | [toplevel] Remove unusable option -notop | Emilio Jesus Gallego Arias | 2017-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. | Maxime Dénès | 2017-03-14 |
|\ \ \ \ \ | |/ / / / |/| | | | | |||
* | | | | | Typo doc notations. | Hugo Herbelin | 2017-03-09 |
| | | | | | |||
* | | | | | Clarifying doc about interpretation of scopes in notations (#5386). | Hugo Herbelin | 2017-03-09 |
| | | | | | |||
| | | * | | Farewell decl_mode | Enrico Tassi | 2017-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. | Hugo Herbelin | 2017-03-03 |
| | | | | |||
* | | | | Adding a file providing extensional choice (i.e. choice over setoids). | Hugo Herbelin | 2017-03-03 |
| | | | | | | | | | | | | | | | | Also integrating suggestions from Théo. | ||
* | | | | Logic library: Adding a characterization of excluded-middle in term of | Hugo Herbelin | 2017-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. | Théo Zimmermann | 2017-02-20 |
|/ / | |||
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-01-19 |
|\| | |||
| * | Fix some typos in tutorial (bug #5294). | Guillaume Melquiond | 2016-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). | Guillaume Melquiond | 2016-12-16 |
| | |