aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/cic.rst
AgeCommit message (Expand)Author
2021-04-10Fix link in doc/cic.rst, there is no Credits chapter anymoreYannick Forster
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
2020-09-30Type{i} should be Type(i).Tanaka Akira
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-13Preserve sections about typing rules in CIC chapter.Théo Zimmermann
2020-05-07Drop some the coqtop output, rephrase a bitQuentin Carbonneaux
2020-05-06Add an example to motivate strictly positive occurrences checkQuentin Carbonneaux
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-03-26Remove outdated mention of -allow-sprop.Théo Zimmermann
2020-03-19Document all the existing attributes.Théo Zimmermann
2019-11-14Fix doc for universes(foo) attributesGaëtan Gilbert
2019-11-08Merge PR #11050: Replace "option" in doc when it refers to a flagThéo Zimmermann
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-11-04Cite POPL19 SProp paperGaëtan Gilbert
2019-10-30Use bullets and indentation (but the result rendering is weird).Théo Zimmermann
2019-10-30Use explicit match as suggested by Clément.Théo Zimmermann
2019-10-30[refman] Add a second example of contradiction when positivity checking is di...Théo Zimmermann
2019-10-30[refman] Give an example of contradiction when positivity checking is disabled.Théo Zimmermann
2019-10-22documentation fixesAntonio Nikishaev
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
2019-03-14Documentation for SPropGaëtan Gilbert
2019-02-20Merge PR #9457: Correct W-Ind in Cic description of the reference manual.Théo Zimmermann
2019-02-19Make the conclusion of local contexts W-Ind empty.Tanaka Akira
2019-02-13Merge PR #9564: Fix small errors in cic.rst (3rd)Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:24:41 +0000