aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Collapse)Author
2018-09-17Add missing index entries.Théo Zimmermann
In particular, this backports e26b67436d12da63a11f0727c5b5895dfd03d249.
2018-09-14Merge PR #7894: Remove quote pluginThéo Zimmermann
2018-09-12Remove quote pluginMaxime Dénès
As far as I know, this plugin is untested and barely maintained. I don't think it has real use cases any more, so let's move it out from the repo and see if somebody wants to take over and maintain it. We also remove the documentation, which was telling our users to look at ring to see an example of reification done using quote, when in fact it wasn't using it anymore.
2018-09-12Manual: fix documentation of the “fresh” tacticVincent Laporte
2018-09-11Grammar entry for the ssr syntax for anonymous arguments.Assia Mahboubi
2018-09-06Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.Pierre-Marie Pédrot
2018-08-31Merge PR #8170: Don't index names starting with `_` in docsThéo Zimmermann
2018-08-31Fixed the seealso directive in a few places.Zeimer
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵Zeimer
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
2018-08-29Merge PR #8353: [sphinx] Fix timeout issue by splitting imports.Clément Pit-Claudel
2018-08-29Merge PR #8345: Add index for focusing braces.Clément Pit-Claudel
2018-08-29[sphinx] Fix timeout issue by splitting imports.Théo Zimmermann
2018-08-28Merge PR #8135: Sphinx fixing of the beginning of the Tactics chapter.Clément Pit-Claudel
2018-08-28Add index for focusing braces.Théo Zimmermann
And fix wrong indentation.
2018-08-27Document focusing on named goals.Théo Zimmermann
2018-08-24Merge PR #8266: Minor Sphinx improvements in the bullet documentation.Clément Pit-Claudel
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-22Add missing spaces.Théo Zimmermann
2018-08-22[sphinx] Improve Case analysis and induction section.Théo Zimmermann
2018-08-22[refman] Fixing two nested lemma errors.Théo Zimmermann
2018-08-22[sphinx] Fixing of the beginning of the Tactics chapter.Théo Zimmermann
2018-08-17Define bullet production token.Théo Zimmermann
2018-08-17Minor Sphinx improvements in the bullet documentation.Théo Zimmermann
And fixing a problem with nested proofs.
2018-08-16Merge PR #8109: [doc] Fix grammar of goal selectors.Maxime Dénès
2018-08-16Merge PR #8108: A few Sphinx fixes in the Ltac chapter.Maxime Dénès
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines.
2018-07-28Merge PR #8077: Fix #7291: unify tactic should have more descriptive error ↵Hugo Herbelin
messages.
2018-07-26[sphinx] Do name cleanup in handle_signatureClément Pit-Claudel
2018-07-25Doc: preliminary work before #7291 which add an "Unable to unify" message.Hugo Herbelin
We adopt the convention that error messages with a template use the sphinx syntax used in defining syntax rules.
2018-07-24Update the documentation w.r.t. the new error raised by unify.Pierre-Marie Pédrot
2018-07-21Solved problems with snippets giving errors in chapter 'Detailed examples of ↵Zeimer
tactics' of the Reference Manual. Refreshed the section on the cardinality of the naturals. Removed the mention of specialize_eqs as it seems very bugged.
2018-07-21Rewrote examples about permutations, logic and type isomorphisms: changed ↵Zeimer
the formatting and renamed the tactics to match modern naming conventions.
2018-07-21Improvements for the chapter 'Detailed examples of tactics' of the Reference ↵Zeimer
Manual.
2018-07-21Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵Théo Zimmermann
and 'Tactics' of the Reference Manual.
2018-07-21Fixing capital letters in the "in" syntax of instantiate.Hugo Herbelin
This trace of V7 syntax remained unnoticed (since July 2004).
2018-07-21[doc] Fix grammar of goal selectors.Théo Zimmermann
2018-07-21A few Sphinx fixes in the Ltac chapter.Théo Zimmermann
Including using subscripts more often.
2018-07-20Small improvements suggested in comments to PR #8086.Zeimer
2018-07-20Improved chapter 'The tactic language' of the Reference Manual.Zeimer
2018-07-20Added :undocumented: and :cmd: as suggested in comments for PR #8072.Zeimer
2018-07-20Fixed 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-17Remove fourier pluginMaxime Dénès
As stated in the manual, the fourier tactic is subsumed by lra.
2018-07-10fixed typo for assert_suceedcharguer
2018-07-10Merge PR #8028: Fix a few typosThéo Zimmermann
2018-07-10Fix typo in doc/proof-engine/tactics.rst.whitequark
2018-07-09Fix rst syntax for `quote ident {ident}`Joachim Breitner
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu 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 {}/viewEnrico Tassi
2018-06-22[ssr] document rewrite {}fooEnrico Tassi
It was used in some examples, but never fully documented
2018-06-21Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 20:11:53 +0000