| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-30 | Remove doc/refman/RefMan-ind.tex | Jason Gross | |
| It does not seem to be referred to by any file, and does not seem to be built by any implicit rules. | |||
| 2017-06-19 | Merge PR#777: Improving documentation of tactic "move" (report #4561) | Maxime Dénès | |
| 2017-06-16 | Document cumulativity for inductive types | Amin Timany | |
| 2017-06-14 | Merge PR#765: Remove obsolete Show commands | Maxime Dénès | |
| 2017-06-14 | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey | |
| 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. | |||
| 2017-06-13 | Improving documentation of tactic "move" (report #4561). | Hugo Herbelin | |
| 2017-06-12 | Remove commented documentation for Show Tree. | Théo Zimmermann | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |