| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-01 | Merge PR#449: make specialize smarter (bug 5370). | Maxime Dénès | |
| 2017-05-31 | Documenting the new behaviour of specialize. | Pierre Courtieu | |
| 2017-05-30 | Documentation for eassert, eenough, epose proof, eset, eremember, epose. | Hugo Herbelin | |
| Includes fixes and suggestions from Théo. | |||
| 2017-05-27 | Documenting the existence of first and solve as Ltac definitions. | Pierre-Marie Pédrot | |
| 2017-05-25 | Merge PR#406: coq makefile2 | Maxime Dénès | |
| 2017-05-23 | add the only target | Enrico Tassi | |
| This makes the following work correctly: make only TGTS="foo bar" -j2 note that make foo bar -j2 is not doing what you think | |||
| 2017-05-23 | enters coq_makefile2 | Enrico Tassi | |
| 2017-05-23 | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias | |
| 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... | |||
| 2017-05-23 | [vernac] Remove `Save.` command. | Emilio Jesus Gallego Arias | |
| It has been deprecated for a while in favor of `Qed`. | |||
| 2017-05-17 | Documenting relaxing of constraints on injection. | Hugo Herbelin | |
| We seized this opportunity to do a little refreshing of the section describing injection. | |||
| 2017-05-17 | 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-11 | 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-04 | Improve documentation of assert / pose proof / specialize. | Théo Zimmermann | |
| 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 | |||
| 2017-05-03 | 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-01 | More consistent writing of de Bruijn. | Théo Zimmermann | |
| 2017-05-01 | Fix for bug 5507. Mispelt de Bruijn. | Théo Zimmermann | |
| 2017-04-28 | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵ | Maxime Dénès | |
| let-ins | |||
| 2017-04-27 | fix order of command-line arguments mentioned in Add LoadPath | Paul Steckler | |
| 2017-04-25 | Mark transparent_abstract as risky in docs | Jason Gross | |
| As per Enrico's request. | |||
| 2017-04-25 | Add transparent_abstract tactic | Jason Gross | |
| 2017-04-24 | refman: remember the old name of template polymorphism. | Gaetan Gilbert | |
| 2017-04-12 | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵ | Maxime Dénès | |
| record fields. | |||
| 2017-04-11 | 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 | |
| Since About mentions it the doc should as well. | |||
| 2017-04-09 | Merge PR#460: Turning the printing primitive projection compatibility flag ↵ | Maxime Dénès | |
| off by default | |||
| 2017-04-09 | Fixing #5420 as well as many related bugs due to miscounting let-ins. | Hugo Herbelin | |
| - 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. | |||
| 2017-04-07 | 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-06 | Merge PR#455: Farewell decl_mode | Maxime Dénès | |
| 2017-03-23 | Documenting the grammar {| ... |} syntax for building records. | Hugo Herbelin | |
| And an extra minor changes (use of zeroone when relevant, use of type rather than term). | |||
| 2017-03-23 | Merge PR#433: doc: fix a French-ism | Maxime Dénès | |
| 2017-03-22 | Fix some typos. | Guillaume Melquiond | |
| 2017-03-22 | Merge PR#482: [toplevel] Remove unusable option -notop | Maxime Dénès | |
| 2017-03-17 | Document Show Match, add ref to that in match variants/extensions | Paul Steckler | |
| 2017-03-14 | doc: fix a French-ism | Valentin Robert | |
| 2017-03-14 | [toplevel] Remove unusable option -notop | Emilio Jesus Gallego Arias | |
| 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 . | |||
| 2017-03-14 | Merge PR#438: Fix V7 syntax in refman. | Maxime Dénès | |
| 2017-03-09 | Typo doc notations. | Hugo Herbelin | |
| 2017-03-09 | Clarifying doc about interpretation of scopes in notations (#5386). | Hugo Herbelin | |
| 2017-03-07 | Farewell decl_mode | Enrico Tassi | |
| This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests. | |||
| 2017-02-20 | Fix V7 syntax in refman. | Théo Zimmermann | |
| 2017-01-19 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-12-16 | Fix incorrect documentation that prevents successful compilation (bug #5265). | Guillaume Melquiond | |
| 2016-12-07 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |