| Commit message (Expand) | Author | Age |
* | [sphinx] Fix missing indices warnings. | Théo Zimmermann | 2018-06-05 |
* | [ssr] index entry for "without loss", "suffices" and "generally have" | Enrico Tassi | 2018-06-05 |
* | [ssr] some fixes to the documentation markup | Enrico Tassi | 2018-06-05 |
* | [sphinx] Start fixing SSR chapter. | Théo Zimmermann | 2018-06-05 |
* | Merge PR #7229: Deprecate implicit tactic solving. | Hugo Herbelin | 2018-06-04 |
|\ |
|
* \ | Merge PR #7601: Fix notation for code snippet in documentation | Maxime Dénès | 2018-06-04 |
|\ \ |
|
| | * | Documenting the deprecation. | Pierre-Marie Pédrot | 2018-06-04 |
| |/
|/| |
|
* | | Merge PR #7648: Indicate in the doc that clearbody can take several idents | Maxime Dénès | 2018-06-04 |
|\ \ |
|
| * | | Merge two clearbody docs | Théo Winterhalter | 2018-06-01 |
| * | | Indicate in the doc that clearbody can take several idents | Théo Winterhalter | 2018-05-31 |
* | | | [doc] Allow more than one signature and name per Sphinx object | Clément Pit-Claudel | 2018-05-25 |
|/ / |
|
| * | Fix notation for code snippet in documentation | Anton Trunov | 2018-05-25 |
|/ |
|
* | Merge PR #7508: Improve rewrite section in tactic chapter. | Maxime Dénès | 2018-05-25 |
|\ |
|
* | | Document nested proofs and associated option. | Théo Zimmermann | 2018-05-17 |
* | | Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter. | Maxime Dénès | 2018-05-16 |
|\ \ |
|
| | * | [sphinx] Fix mistake in index. | Théo Zimmermann | 2018-05-16 |
| | * | [sphinx] Improve rewrite section in tactic chapter. | Théo Zimmermann | 2018-05-16 |
| |/
|/| |
|
* | | [doc] Small fixes | Clément Pit-Claudel | 2018-05-15 |
| * | [sphinx] Fix indentation at the end of proof handling chapter. | Théo Zimmermann | 2018-05-15 |
|/ |
|
* | Remove duplicate entries for Proof, Qed, Defined, Admitted. | Théo Zimmermann | 2018-05-14 |
* | Merge PR #7374: [sphinx] More fatal warnings. | Maxime Dénès | 2018-05-14 |
|\ |
|
* | | Doc: Renaming an old-style numerical evar in an alphabetical one. | Hugo Herbelin | 2018-05-11 |
* | | Doc: Moving `\forall` to `forall` in file tactics.rst. | Hugo Herbelin | 2018-05-11 |
* | | Doc: Some quotes missing in file tactics.rst. | Hugo Herbelin | 2018-05-11 |
* | | Replacing a broken reference by hyperlinks in chapter tactics. | Hugo Herbelin | 2018-05-11 |
* | | A few fixes in chapter tactics. | Hugo Herbelin | 2018-05-11 |
* | | [sphinx] Improve proof handling chapter. | Théo Zimmermann | 2018-05-09 |
* | | Clarify that the description of coqtop does not reflect all user interfaces. | Théo Zimmermann | 2018-05-09 |
* | | [sphinx] Improvements around the Show commands, including missing indices and... | Théo Zimmermann | 2018-05-09 |
| * | [sphinx] Fix new warnings related to tacn, cmd, opt... | Théo Zimmermann | 2018-05-09 |
| * | Replacing a broken reference by hyperlinks in chapter tactics. | Hugo Herbelin | 2018-05-09 |
| * | A few fixes in chapter tactics. | Hugo Herbelin | 2018-05-09 |
|/ |
|
* | [sphinx] Fixes around apply, including indentation and fixing a Coq warning. | Théo Zimmermann | 2018-05-05 |
* | [sphinx] Fixes around refine, including indentation and a hard-coded ref. | Théo Zimmermann | 2018-05-05 |
* | [sphinx] Add indices for only, all and par. | Théo Zimmermann | 2018-05-05 |
* | [sphinx] Improvements around injection tactic. | Théo Zimmermann | 2018-05-05 |
* | [sphinx] Improve part about Hints. | Théo Zimmermann | 2018-05-05 |
* | [sphinx] Re-indent to get much better rendering. | Théo Zimmermann | 2018-05-05 |
* | Clean-up around cmd documentation. | Théo Zimmermann | 2018-05-05 |
* | Remove duplicate Extraction commands documentation. | Théo Zimmermann | 2018-05-05 |
* | [sphinx] Replace remaining `@natural` by `@num`. | Théo Zimmermann | 2018-05-05 |
* | [sphinx] Use references for command Info. | Théo Zimmermann | 2018-05-05 |
* | [sphinx] More reference fixes. | Théo Zimmermann | 2018-05-05 |
* | [sphinx] Use references for Print. | Théo Zimmermann | 2018-05-05 |
* | Fix error messages and make them consistent. | Théo Zimmermann | 2018-05-05 |
* | Add direct reference to congruence with. | Théo Zimmermann | 2018-05-05 |
* | Clean-up around options. | Théo Zimmermann | 2018-05-05 |
* | debug trivial and debug auto were not in the tactic index. | Théo Zimmermann | 2018-05-05 |
* | [sphinx] Fix some references. | Théo Zimmermann | 2018-05-05 |
* | [sphinx] Backport reformulation. | Théo Zimmermann | 2018-05-05 |