Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Added :undocumented: and :cmd: as suggested in comments for PR #8072. | 2018-07-20 | |
| | |||
* | Fixed many spelling and grammar errors in the chapters 'Vernacular ↵ | 2018-07-20 | |
| | | | | | | | commands', 'Proof handling' and 'Tactics' of the Reference Manual. Fixed some more serious errors related to tactics functional induction, unfold, hnf and red. Added some error messages and remarks for tactics btauto, rtauto and red. | ||
* | Remove fourier plugin | 2018-07-17 | |
| | | | | As stated in the manual, the fourier tactic is subsumed by lra. | ||
* | Merge PR #8028: Fix a few typos | 2018-07-10 | |
|\ | |||
| * | Fix typo in doc/proof-engine/tactics.rst. | 2018-07-10 | |
| | | |||
* | | Fix rst syntax for `quote ident {ident}` | 2018-07-09 | |
|/ | |||
* | hints: add Hint Variables/Constants Opaque/Transparent commands | 2018-07-02 | |
| | | | | | | | | | | | This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables | ||
* | Fix #7421: constr_eq ignores universe constraints. | 2018-06-18 | |
| | | | | | The test isn't quite the one in #7421 because that use of algebraic universes is wrong. | ||
* | A few additional small fixes. | 2018-06-05 | |
| | |||
* | Merge PR #7229: Deprecate implicit tactic solving. | 2018-06-04 | |
|\ | |||
* \ | Merge PR #7601: Fix notation for code snippet in documentation | 2018-06-04 | |
|\ \ | |||
| | * | Documenting the deprecation. | 2018-06-04 | |
| |/ |/| | |||
* | | Merge two clearbody docs | 2018-06-01 | |
| | | |||
* | | Indicate in the doc that clearbody can take several idents | 2018-05-31 | |
| | | |||
| * | Fix notation for code snippet in documentation | 2018-05-25 | |
|/ | | | | It failed to compile before because the type arguments were declared implicit after introducing the notation | ||
* | [sphinx] Fix mistake in index. | 2018-05-16 | |
| | |||
* | [sphinx] Improve rewrite section in tactic chapter. | 2018-05-16 | |
| | | | | Including a fix to the example given in #7407. | ||
* | [doc] Small fixes | 2018-05-15 | |
| | |||
* | Merge PR #7374: [sphinx] More fatal warnings. | 2018-05-14 | |
|\ | |||
* | | Doc: Renaming an old-style numerical evar in an alphabetical one. | 2018-05-11 | |
| | | |||
* | | Doc: Moving `\forall` to `forall` in file tactics.rst. | 2018-05-11 | |
| | | | | | | | | | | Not only are most of "forall"s in the manual in Coq notation, but the math notation leads to have a specially long space after the comma. | ||
* | | Doc: Some quotes missing in file tactics.rst. | 2018-05-11 | |
| | | |||
* | | Replacing a broken reference by hyperlinks in chapter tactics. | 2018-05-11 | |
| | | |||
* | | A few fixes in chapter tactics. | 2018-05-11 | |
| | | |||
| * | [sphinx] Fix new warnings related to tacn, cmd, opt... | 2018-05-09 | |
| | | |||
| * | Replacing a broken reference by hyperlinks in chapter tactics. | 2018-05-09 | |
| | | |||
| * | A few fixes in chapter tactics. | 2018-05-09 | |
|/ | |||
* | [sphinx] Fixes around apply, including indentation and fixing a Coq warning. | 2018-05-05 | |
| | |||
* | [sphinx] Fixes around refine, including indentation and a hard-coded ref. | 2018-05-05 | |
| | |||
* | [sphinx] Improvements around injection tactic. | 2018-05-05 | |
| | |||
* | [sphinx] Improve part about Hints. | 2018-05-05 | |
| | | | | Fix Hint (Transparent | Opaque) index. | ||
* | Clean-up around cmd documentation. | 2018-05-05 | |
| | | | | In particular, remove trailing dots. | ||
* | [sphinx] More reference fixes. | 2018-05-05 | |
| | |||
* | Fix error messages and make them consistent. | 2018-05-05 | |
| | | | | All the error messages start with a capitalized letter and end with a dot. | ||
* | Add direct reference to congruence with. | 2018-05-05 | |
| | |||
* | Clean-up around options. | 2018-05-05 | |
| | | | | | | - Remove all trailing dots. - There is only one Bullet Behavior option. - Replaces `@natural` and `@integer` by `@num`. | ||
* | debug trivial and debug auto were not in the tactic index. | 2018-05-05 | |
| | |||
* | [sphinx] Backport reformulation. | 2018-05-05 | |
| | | | | (cf. 711b9d8cdf6e25690d247d9e8c49f005527e64e2) | ||
* | Make "intro"/"intros" progress on existential variables. | 2018-05-02 | |
| | |||
* | Strict focusing using Default Goal Selector. | 2018-04-29 | |
| | | | | | | | | | | | | We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689. | ||
* | [Sphinx] Clean-up indices | 2018-04-16 | |
| | |||
* | [Sphinx] Fix a lot of references and description of options | 2018-04-16 | |
| | |||
* | [Sphinx] Fix all remaining warnings. | 2018-04-14 | |
| | |||
* | [sphinx] Fix many warnings. | 2018-04-14 | |
| | | | | | Including cross-reference TODOs. I took down the number of warnings from 300 to 50. | ||
* | Clarify wording in tactics documentation. | 2018-03-25 | |
| | | | | Closes #6980. | ||
* | [Sphinx] Add chapter 8 | 2018-03-15 | |
| | | | | Thanks to Heiko Becker and Nikita Zyuzin for porting this chapter. | ||
* | [Sphinx] Move chapter 8 to new infrastructure | 2018-03-15 | |