aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
AgeCommit message (Expand)Author
2019-01-31Use λ instead of \lb.Tanaka Akira
2019-01-31The subst Γ{c}{(c c')} should be Γ{c'}{(c' c)}.Tanaka Akira
2019-01-31Use "U" instead of "u" for a type.Tanaka Akira
2019-01-31Fix an index. The number of constructors is "l".Tanaka Akira
2019-01-31Use \Match for match construct.Tanaka Akira
2019-01-31Insert a space before \kwend.Tanaka Akira
2019-01-31Use \length for the function name of length.Tanaka Akira
2019-01-31Adjust spaces.Tanaka Akira
2019-01-31Use "∀" and "λ" instead of \forall and \lambda.Tanaka Akira
2019-01-31Use math more.Tanaka Akira
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-28Merge PR #9402: Move \def\plus and \def\tri to refman-preamble.sty.Théo Zimmermann
2019-01-25Merge PR #9391: Clarify meaning of Primitive ProjectionsThéo Zimmermann
2019-01-25Move \def\plus and \def\tri to refman-preamble.sty.Tanaka Akira
2019-01-24Merge PR #9269: Move and rewrite intro pattern sectionThéo Zimmermann
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-22Remove unneeded | in productionlistsJim Fehrle
2019-01-10Remove Printing Primitive Projection CompatibilityGaëtan Gilbert
2019-01-08Add doc for auto-template warningGaëtan Gilbert
2018-12-19Fix typo in gallina specification language docyudetamago
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try t...Théo Zimmermann
2018-11-30Add indexes for coercion / substructure symbol :>.Théo Zimmermann
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
2018-11-19Merge PR #8451: Print Universes SubgraphPierre-Marie Pédrot
2018-11-16Print Universes SubgraphGaëtan Gilbert
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-10-29Fix typos in the document about CICwkwkes
2018-10-23Order Greek letters consistently w/rest of documentSam Pablo Kuper
2018-10-16Document the issue with positive coinductive types.Pierre-Marie Pédrot
2018-10-10Merge PR #8384: Small fixes in attribute documentation.Clément Pit-Claudel
2018-10-01Docs: Missing backquoteJoachim Breitner
2018-09-28Small fixes in attribute documentation.Théo Zimmermann
2018-09-26Allow successive attributes #[foo] #[bar]Gaëtan Gilbert
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
2018-09-20[doc] Fix more duplicate-label issues in production listsClément Pit-Claudel
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-20[doc] Fix a few LaTeX mistakesClément Pit-Claudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:42:06 +0000