aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
AgeCommit message (Expand)Author
2019-03-13[refman] Remove warning silencing by fixing the underlying issue.Théo Zimmermann
2019-03-13[refman] Fix other newly emitted warnings.Théo Zimmermann
2019-03-12[refman] Add 'warn' option to coqtop directive.Théo Zimmermann
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
2019-03-10Merge PR #9654: [sphinx] Add warn option to coqtop directive.Clément Pit-Claudel
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-28[sphinx] Add warn option to coqtop directive.Théo Zimmermann
2019-02-25[Manual] Document primitive integersVincent Laporte
2019-02-20Merge PR #9457: Correct W-Ind in Cic description of the reference manual.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-22 03:37:47 +0000