aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2019-01-31Make parenthesis correctly matched.Tanaka Akira
2019-01-31\Sort is not a term.Tanaka Akira
2019-01-31Use semicolon for separator of local contexts.Tanaka Akira
2019-01-31Don't line break at hyphen of compound words.Tanaka Akira
2019-01-31Move out a period and comma from :math:.Tanaka Akira
2019-01-31Nest :math: and parenthesis properly.Tanaka Akira
2019-01-31Fix syntax of two lambda-abstractions.Tanaka Akira
2019-01-31Change {\Sort} to \Sort.Tanaka Akira
2019-01-31Use \Prop, \Set and \Type defined in refman-preamble.sty.Tanaka Akira
2019-01-31Make "1" and "2" in "f1" and "f2" suffixes.Tanaka Akira
2019-01-31Make "1" and "n" in "u1" and "un" suffixes.Tanaka Akira
2019-01-31Remove "End TreeExample." line.Tanaka Akira
2019-01-31Merge PR #8720: [Numeral notations] Use Coqlib registered constantsEmilio Jesus Gallego Arias
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2019-01-29Use \mathcal instead of \calGaëtan Gilbert
2019-01-28Surround "assumption" with :tacn:`` in tactics.rstRyan Scott
2019-01-28Merge PR #9402: Move \def\plus and \def\tri to refman-preamble.sty.Théo Zimmermann
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
2019-01-25Merge PR #9391: Clarify meaning of Primitive ProjectionsThéo Zimmermann
2019-01-25[Numeral notations] Lazy resolution of decimal typesVincent Laporte
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_div...Jason Gross
2019-01-24Revert "Add subst to the end of nia in the test-suite"Jason Gross
2019-01-24Add subst to the end of nia in the test-suiteJason Gross
2019-01-24Don't bundle Z.div_mod_quot_rem into zifyJason Gross
2019-01-24Add Z.div_mod_to_quot_rem tactic, put it in zifyJason Gross
2019-01-24Update -compat to support -compat 8.10Jason Gross
2019-01-25Move \def\plus and \def\tri to refman-preamble.sty.Tanaka Akira
2019-01-24Merge PR #9384: Improve the note in the beginning of the Ltac chapter.Clément Pit-Claudel
2019-01-24Merge PR #9269: Move and rewrite intro pattern sectionThéo Zimmermann
2019-01-24Merge PR #9392: Fix small errors in cic.rst.Théo Zimmermann
2019-01-24[doc] warn that (automatic) clears can result in errorsEnrico Tassi
2019-01-24[doc] more precise description of when automatic clears are triggeredEnrico Tassi
2019-01-24[doc] explain how to avoid automatic clearsEnrico Tassi
2019-01-24use \nO, \nS, etc. fix \kw{n}.Tanaka Akira
2019-01-24Fix small errors in cic.rst.Tanaka Akira
2019-01-23Clarify meaning of Primitive ProjectionsDavid A. Dalrymple
2019-01-23Move and rewrite documentation for intro patterns that was underJim Fehrle
2019-01-23Fix the information of the level of ; vs ; [ ]Théo Zimmermann
2019-01-23Improve the note in the beginning of the Ltac chapter.Théo Zimmermann
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2019-01-22clarify when an ident is added to the clear switchEnrico Tassi
2019-01-22Apply suggestions from code reviewThéo Zimmermann
2019-01-21ring and field simplify can take no argumentsthery
2019-01-21[ssr] better structure the ipats docEnrico Tassi
2019-01-21Merge PR #9304: Default disable auto template warning.Maxime Dénès
2019-01-19[ssr] compile "=> {x..} y" as "=> {x..y} y"Enrico Tassi
2019-01-18[ssr] compile "=> {} y" as "=> {y} y"Enrico Tassi
2019-01-11Merge pull request #8778 from SkySkimmer/merge-plugin-tutoYves Bertot
2019-01-10Remove Printing Primitive Projection CompatibilityGaëtan Gilbert
2019-01-09[Manual] Remove link to non-existing CSS fileVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 08:01:13 +0000