| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-15 | [Sphinx] Move chapter 8 to new infrastructure | Maxime Dénès | |
| 2018-03-08 | [compat] Remove "Refolding Reduction" option. | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove support refolding in reduction. We also update a test case that was not properly understood, see the discussion in #6895. | |||
| 2018-03-06 | Merge PR #6898: [compat] Remove "Intuition Iff Unfolding" | Maxime Dénès | |
| 2018-03-04 | Merge PR #915: Fix rewrite in * side conditions | Maxime Dénès | |
| 2018-03-03 | [compat] Remove "Intuition Iff Unfolding" | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove the option "Intuition Iff Unfolding" | |||
| 2018-03-01 | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". | Hugo Herbelin | |
| Noticed by Sigurd Schneider. | |||
| 2018-02-27 | Typo in the documentation of the `pattern` tactic | Joachim Breitner | |
| 2017-12-14 | Add doc for Set Debug RAKAM. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Debug Cbv. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Info/Debug Auto/Trivial/Eauto. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Congruence Verbose | Gaëtan Gilbert | |
| 2017-10-24 | Fix #4846 | Johannes Kloos | |
| Bug description: The "now" tactic, which is being used in the standard library, is not documented in the Reference Manual This commit documents the easy tactic, and gives now as a variant. | |||
| 2017-10-24 | Fix #5413: [unfold ... in] not documented | Johannes Kloos | |
| Made a description of unfold...in and moved the index entry there. | |||
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond | |
| 2017-09-01 | add option index entry for NativeCompute Profiling | Paul Steckler | |
| 2017-08-18 | use OCaml temp_file, instead of our own version | Paul Steckler | |
| 2017-08-17 | Add native compute profiling, BZ#5170 | Paul Steckler | |
| 2017-08-16 | mention that tactic is the identity or gives error | Paul Steckler | |
| 2017-08-16 | change section caption, improve some wording | Paul Steckler | |
| 2017-07-28 | Fix documentation of Hint Mode (bug #4911). | Guillaume Melquiond | |
| 2017-07-11 | Sync the manual with the deprecation warnings. | Théo Zimmermann | |
| 2017-07-05 | Merge PR #837: Add inversion_sigma to CHANGES and to doc | Maxime Dénès | |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-06-30 | Add doc for inversion_sigma to RefMan-tac | Jason Gross | |
| 2017-06-19 | Merge PR#777: Improving documentation of tactic "move" (report #4561) | 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-13 | Document instantiate (ident := term) and make it the preferred variant. | 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-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-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-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. | |||
| 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-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-07 | Merge remote-tracking branch 'github/pr/339' into v8.6 | Maxime Dénès | |
| Was PR#339: Documenting type class options, typeclasses eauto | |||
| 2016-11-07 | Document two new variants of refine | Matthieu Sozeau | |
| They allow to call refine without doing typeclass resolution, allowing to use refine in typeclass hints. | |||
| 2016-11-05 | Minor fix in documentation | Matthieu Sozeau | |
| 2016-11-04 | Merge remote-tracking branch 'github/pr/336' into v8.6 | Maxime Dénès | |
| Was PR#336: Remove v62 | |||
| 2016-11-03 | Lets Hints/Instances take an optional pattern | Matthieu Sozeau | |
| In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well. | |||
| 2016-10-29 | Documenting changes in typeclasses | Matthieu Sozeau | |
| 2016-10-25 | Remove v62 from the refman. | Théo Zimmermann | |
| 2016-10-24 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-19 | Documenting Hint Resolve -> and <- variants. | Théo Zimmermann | |
| These variants are from 8.3 but were never documented except in CHANGES. | |||
| 2016-10-19 | Making the doc of auto hints more precise. | Théo Zimmermann | |
| The doc of auto hints now mention again that sometimes a hint will be used with simple apply and sometimes it will be used with exact. It does not try to be fully precise in that we don't necessarily want to document the behaviors of auto that we might like to change. See also the discussion on commit 9227d6e. | |||
| 2016-10-18 | Extending the doc with a general summary of auto variants. | Théo Zimmermann | |
| This way of giving the summary avoids redundancy as much as possible. It is helpful for the auto-completion of Company-Coq of @cpitclaudel. | |||
| 2016-10-18 | Document info_auto. | Théo Zimmermann | |
| Now that this tactic has been fixed (commit 58d1381), it needed to get documented. | |||
| 2016-10-18 | Improve the documentation of eauto. | Théo Zimmermann | |
| Improve the description of what auto/eauto do. These two tactics rely on the simple version of apply/eapply. Since this simple version is available to the end user, it is better to mention it. See also the confusion that such description can create in the thread "Understanding auto" on Coq-Club. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |