aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
AgeCommit message (Expand)Author
2019-02-19Merge PR #9501: Sphinx: fail when a command fails + other stuffClément Pit-Claudel
2019-02-19Make the conclusion of local contexts W-Ind empty.Tanaka Akira
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-18Using options abort and restart of coqtop directive in the manual.Théo Zimmermann
2019-02-13Merge PR #9450: Fix #9432: canonical structure and coercion accept universe b...Maxime Dénès
2019-02-13[ssr] move shorter Canonical to Coq properEnrico Tassi
2019-02-13Merge PR #9564: Fix small errors in cic.rst (3rd)Théo Zimmermann
2019-02-12Fix failing coqtops in gallina-specification-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in gallina-extensions.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in coq-library.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in cic.rstGaëtan Gilbert
2019-02-11Use math mode more.Tanaka Akira
2019-02-11Use {LEFT,RIGHT} DOUBLE QUOTATION MARK.Tanaka Akira
2019-02-11Remove a space before closing double-quote.Tanaka Akira
2019-02-10Change "I" to "I_p".Tanaka Akira
2019-02-10Distinguish inductive {definition,inductive}.Tanaka Akira
2019-02-08Use math mode more.Tanaka Akira
2019-02-08Fix index of arguments of constructor in fixpoint.Tanaka Akira
2019-02-08Change parameters p_1...p_r to q_1...q_r.Tanaka Akira
2019-02-08Change the index "p" to "s" in "type of branches".Tanaka Akira
2019-02-08Change c to c' forgotten at exchanging c and c'.Tanaka Akira
2019-02-08Remove spaces just before period (non-math mode).Tanaka Akira
2019-02-08Remove spaces just before comma (non-math mode).Tanaka Akira
2019-02-08Remove "'" accidentaly added.Tanaka Akira
2019-02-01Correct W-Ind.Tanaka Akira
2019-02-01The lowest universe level is 1.Tanaka Akira
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-14 08:25:38 +0000