| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-11 | Add documentation for Set Ltac Batch Debug | Jason Gross | |
| 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-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-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 | |
| 2016-12-06 | Fix broken documentation in presence of \zeroone{... \tt ...}. | Guillaume Melquiond | |
| The way \zeroone was defined, the \tt modifier was leaked outside the brackets, thus messing with the following text. There are a bunch of occurrences of this issue in the manual, so rather than turning all the \tt into \texttt, the definition of \zeroone is made more robust. Unfortunately, there is one single occurrence of \zeroone that does not support the more robust version. (Note that this specific usage of \zeroone is morally a bug, since it goes against all the LaTeX conventions.) So the commit also keeps the old leaky version of \zeroone around as \zeroonelax so that it can be used there. | |||
| 2016-12-06 | Update documentation (bugs #5246 and #5251). | Guillaume Melquiond | |
| 2016-12-05 | Change module for Coq loop | Paul Steckler | |
| 2016-12-05 | the -byte option is deprecated | Paul Steckler | |
| 2016-11-18 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-11-17 | Add missing label. Fixes broken ref. | Théo Zimmermann | |
| 2016-11-16 | Revert more of a477dc for good measure | Matthieu Sozeau | |
| We stop failing automatically on non-declared-class nested or toplevel subgoals as in 8.5, instead of the previous a477dc behavior of shelving those goals and failing if shelved goals remained at the end of resolution. It means typeclass resolution during refinement is closer to all:typeclasses eauto. Hints in typeclass_instances for non-declared classes can be used during resolution of _nested_ subgoals when it is fired from type-inference, toplevel goals considered in this case are still only classes (as in 8.5 and before). The code that triggers the restriction to only declared class subgoals is commented. Revert changes to test-suite, adding test for #5203, #5198 is fixed too. Add corresponding tests in the test-suite (that will break if we, e.g. disallow non-class subgoals) and update the refman accordingly. | |||
| 2016-11-15 | Revert part of a477dc, disallow_shelved | Matthieu Sozeau | |
| In only_classes mode we do not try to implement a stricter semantics for shelved goals in 8.6. Leaving this for 8.7. Update the documentation as well. Remove a spurious printf call as well. Fix test-suite now that shelved goals are allowed | |||
| 2016-11-14 | Do not mention "none" in warnings doc, as it is there for compatibility. | Maxime Dénès | |
| 2016-11-10 | Update CHANGES and credits for 8.6beta1. | Maxime Dénès | |
| 2016-11-08 | Merge remote-tracking branch 'github/pr/348' into v8.6 | Maxime Dénès | |
| Was PR#348: Credits for 8.6 | |||
| 2016-11-08 | Update documentation of Arguments after recent changes. | Maxime Dénès | |
| 2016-11-08 | Rewording from Enrico | Matthieu Sozeau | |
| 2016-11-07 | After Emilio's comment. | Matthieu Sozeau | |
| 2016-11-07 | Merge remote-tracking branch 'github/pr/339' into v8.6 | Maxime Dénès | |
| Was PR#339: Documenting type class options, typeclasses eauto | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |