Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | fixed typo for assert_suceed | 2018-07-10 | |
| | |||
* | 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 | ||
* | [ssr] document {}/view | 2018-06-22 | |
| | |||
* | [ssr] document rewrite {}foo | 2018-06-22 | |
| | | | | It was used in some examples, but never fully documented | ||
* | Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter. | 2018-06-21 | |
|\ | |||
* \ | Merge PR #7491: Fix #7421: constr_eq ignores universe constraints. | 2018-06-19 | |
|\ \ | |||
| | * | [doc] Fix a typo in the ssreflect chapter | 2018-06-19 | |
| | | | |||
| | * | [doc] Fix uncaught duplicate-label errors in the SSReflect chapter | 2018-06-19 | |
| |/ |/| | |||
| * | 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. | ||
* | | Fix #7829: Spurious documentation failures. | 2018-06-18 | |
|/ | | | | We split a Require Import in two to avoid reaching the timeout. | ||
* | Improve links to SSR tactics, and some other improvements. | 2018-06-05 | |
| | |||
* | Workaround a weird error of .. coqtop:: | 2018-06-05 | |
| | |||
* | Remove many abusive .. coqtop in SSR chapter. | 2018-06-05 | |
| | | | | Many still remain. | ||
* | A few additional small fixes. | 2018-06-05 | |
| | |||
* | [sphinx] Fix missing indices warnings. | 2018-06-05 | |
| | |||
* | [ssr] index entry for "without loss", "suffices" and "generally have" | 2018-06-05 | |
| | |||
* | [ssr] some fixes to the documentation markup | 2018-06-05 | |
| | |||
* | [sphinx] Start fixing SSR chapter. | 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 PR #7648: Indicate in the doc that clearbody can take several idents | 2018-06-04 | |
|\ \ | |||
| * | | Merge two clearbody docs | 2018-06-01 | |
| | | | |||
| * | | Indicate in the doc that clearbody can take several idents | 2018-05-31 | |
| | | | |||
* | | | [doc] Allow more than one signature and name per Sphinx object | 2018-05-25 | |
|/ / | | | | | | | As discussed in GH-7556. | ||
| * | 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 | ||
* | Merge PR #7508: Improve rewrite section in tactic chapter. | 2018-05-25 | |
|\ | |||
* | | Document nested proofs and associated option. | 2018-05-17 | |
| | | |||
* | | Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter. | 2018-05-16 | |
|\ \ | |||
| | * | [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 | |
| | | |||
| * | [sphinx] Fix indentation at the end of proof handling chapter. | 2018-05-15 | |
|/ | |||
* | Remove duplicate entries for Proof, Qed, Defined, Admitted. | 2018-05-14 | |
| | | | | And marginal improvements in the last section of the Gallina chapter. | ||
* | 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] Improve proof handling chapter. | 2018-05-09 | |
| | | |||
* | | Clarify that the description of coqtop does not reflect all user interfaces. | 2018-05-09 | |
| | | |||
* | | [sphinx] Improvements around the Show commands, including missing indices ↵ | 2018-05-09 | |
| | | | | | | | | and indentation. | ||
| * | [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 | |
| |