aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine/tactics.rst
AgeCommit message (Expand)Author
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-12Remove quote pluginMaxime Dénès
2018-09-06Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.Pierre-Marie Pédrot
2018-08-31Fixed the seealso directive in a few places.Zeimer
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...Zeimer
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-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
2018-07-28Merge PR #8077: Fix #7291: unify tactic should have more descriptive error me...Hugo Herbelin
2018-07-25Doc: preliminary work before #7291 which add an "Unable to unify" message.Hugo Herbelin
2018-07-24Update the documentation w.r.t. the new error raised by unify.Pierre-Marie Pédrot
2018-07-21Fixing capital letters in the "in" syntax of instantiate.Hugo Herbelin
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 commands',...Zeimer
2018-07-17Remove fourier pluginMaxime Dénès
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
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
2018-06-05A few additional small fixes.Théo Zimmermann
2018-06-04Merge PR #7229: Deprecate implicit tactic solving.Hugo Herbelin
2018-06-04Merge PR #7601: Fix notation for code snippet in documentationMaxime Dénès
2018-06-04Documenting the deprecation.Pierre-Marie Pédrot
2018-06-01Merge two clearbody docsThéo Winterhalter
2018-05-31Indicate in the doc that clearbody can take several identsThéo Winterhalter
2018-05-25Fix notation for code snippet in documentationAnton Trunov
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-15[doc] Small fixesClément Pit-Claudel
2018-05-14Merge PR #7374: [sphinx] More fatal warnings.Maxime Dénès
2018-05-11Doc: Renaming an old-style numerical evar in an alphabetical one.Hugo Herbelin
2018-05-11Doc: Moving `\forall` to `forall` in file tactics.rst.Hugo Herbelin
2018-05-11Doc: Some quotes missing in file tactics.rst.Hugo Herbelin
2018-05-11Replacing a broken reference by hyperlinks in chapter tactics.Hugo Herbelin
2018-05-11A few fixes in chapter tactics.Hugo Herbelin
2018-05-09[sphinx] Fix new warnings related to tacn, cmd, opt...Théo Zimmermann
2018-05-09Replacing a broken reference by hyperlinks in chapter tactics.Hugo Herbelin
2018-05-09A few fixes in chapter tactics.Hugo Herbelin
2018-05-05[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] Improvements around injection tactic.Théo Zimmermann
2018-05-05[sphinx] Improve part about Hints.Théo Zimmermann
2018-05-05Clean-up around cmd documentation.Théo Zimmermann
2018-05-05[sphinx] More reference fixes.Théo Zimmermann
2018-05-05Fix error messages and make them consistent.Théo Zimmermann
2018-05-05Add direct reference to congruence with.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 18:51:18 +0000