| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-21 | Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵ | Théo Zimmermann | |
| and 'Tactics' of the Reference Manual. | |||
| 2018-07-20 | Small improvements suggested in comments to PR #8086. | Zeimer | |
| 2018-07-20 | Improved chapter 'The tactic language' of the Reference Manual. | Zeimer | |
| 2018-07-20 | Added :undocumented: and :cmd: as suggested in comments for PR #8072. | Zeimer | |
| 2018-07-20 | Fixed many spelling and grammar errors in the chapters 'Vernacular ↵ | Zeimer | |
| 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. | |||
| 2018-07-17 | Remove fourier plugin | Maxime Dénès | |
| As stated in the manual, the fourier tactic is subsumed by lra. | |||
| 2018-07-10 | fixed typo for assert_suceed | charguer | |
| 2018-07-10 | Merge PR #8028: Fix a few typos | Théo Zimmermann | |
| 2018-07-10 | Fix typo in doc/proof-engine/tactics.rst. | whitequark | |
| 2018-07-09 | Fix rst syntax for `quote ident {ident}` | Joachim Breitner | |
| 2018-07-02 | hints: add Hint Variables/Constants Opaque/Transparent commands | Matthieu Sozeau | |
| 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 | |||
| 2018-06-22 | [ssr] document {}/view | Enrico Tassi | |
| 2018-06-22 | [ssr] document rewrite {}foo | Enrico Tassi | |
| It was used in some examples, but never fully documented | |||
| 2018-06-21 | Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter. | Maxime Dénès | |
| 2018-06-19 | Merge PR #7491: Fix #7421: constr_eq ignores universe constraints. | Pierre-Marie Pédrot | |
| 2018-06-19 | [doc] Fix a typo in the ssreflect chapter | Clément Pit-Claudel | |
| 2018-06-19 | [doc] Fix uncaught duplicate-label errors in the SSReflect chapter | Clément Pit-Claudel | |
| 2018-06-18 | Fix #7421: constr_eq ignores universe constraints. | Gaëtan Gilbert | |
| The test isn't quite the one in #7421 because that use of algebraic universes is wrong. | |||
| 2018-06-18 | Fix #7829: Spurious documentation failures. | Théo Zimmermann | |
| We split a Require Import in two to avoid reaching the timeout. | |||
| 2018-06-05 | Improve links to SSR tactics, and some other improvements. | Théo Zimmermann | |
| 2018-06-05 | Workaround a weird error of .. coqtop:: | Théo Zimmermann | |
| 2018-06-05 | Remove many abusive .. coqtop in SSR chapter. | Théo Zimmermann | |
| Many still remain. | |||
| 2018-06-05 | A few additional small fixes. | Théo Zimmermann | |
| 2018-06-05 | [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-04 | 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-01 | Merge two clearbody docs | Théo Winterhalter | |
| 2018-05-31 | Indicate in the doc that clearbody can take several idents | Théo Winterhalter | |
| 2018-05-25 | [doc] Allow more than one signature and name per Sphinx object | Clément Pit-Claudel | |
| As discussed in GH-7556. | |||
| 2018-05-25 | Fix notation for code snippet in documentation | Anton Trunov | |
| It failed to compile before because the type arguments were declared implicit after introducing the notation | |||
| 2018-05-25 | Merge PR #7508: Improve rewrite section in tactic chapter. | Maxime Dénès | |
| 2018-05-17 | Document nested proofs and associated option. | Théo Zimmermann | |
| 2018-05-16 | 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 | |
| Including a fix to the example given in #7407. | |||
| 2018-05-15 | [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-14 | Remove duplicate entries for Proof, Qed, Defined, Admitted. | Théo Zimmermann | |
| And marginal improvements in the last section of the Gallina chapter. | |||
| 2018-05-14 | Merge PR #7374: [sphinx] More fatal warnings. | Maxime Dénès | |
| 2018-05-11 | 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 | |
| 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. | |||
| 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-09 | [sphinx] Improve proof handling chapter. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |