aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Expand)Author
2018-05-25Merge PR #7508: Improve rewrite section in tactic chapter.Maxime Dénès
2018-05-17Document nested proofs and associated option.Théo Zimmermann
2018-05-16Merge 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-15[doc] Small fixesClément Pit-Claudel
2018-05-15[sphinx] Fix indentation at the end of proof handling chapter.Théo Zimmermann
2018-05-14Remove duplicate entries for Proof, Qed, Defined, Admitted.Théo Zimmermann
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] Improve proof handling chapter.Théo Zimmermann
2018-05-09Clarify 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-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] 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-05Clean-up around cmd documentation.Théo Zimmermann
2018-05-05Remove 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-05Fix error messages and make them consistent.Théo Zimmermann
2018-05-05Add direct reference to congruence with.Théo Zimmermann
2018-05-05Clean-up around options.Théo Zimmermann
2018-05-05debug 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[sphinx] Backport fix of typo.Théo Zimmermann
2018-05-02Make "intro"/"intros" progress on existential variables.Hugo Herbelin
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
2018-04-16Merge PR #7270: Sphinx doc fix indicesMaxime Dénès
2018-04-16[Sphinx] Clean-up indicesMaxime Dénès
2018-04-16Merge PR #7264: [Sphinx] Fix a lot of references and description of optionsMaxime Dénès
2018-04-16[Sphinx] Fix a lot of references and description of optionsMaxime Dénès
2018-04-16Document the Export Set/Unset commands.Pierre-Marie Pédrot
2018-04-14[Sphinx] Fix all remaining warnings.Maxime Dénès
2018-04-14[sphinx] Fix many warnings.Théo Zimmermann
2018-04-14[Sphinx] Add chapter 9.Théo Zimmermann
2018-04-14[Sphinx] Move chapter 9 to new infrastructure.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 04:56:52 +0000