aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum
AgeCommit message (Expand)Author
2019-05-10[Attributes] Allow explicit value for two-valued attributesVincent Laporte
2019-05-10[User manual] Fix two warnings related to canonical structuresVincent Laporte
2019-05-02Fix #5752: `Hint Mode` ignored for type classes that appear as assumptionsMaxime Dénès
2019-04-30First fixing pass, and experiment with dune-style PR number and author listing.Théo Zimmermann
2019-04-27Minor doc improvement.Théo Zimmermann
2019-04-27[refman] Fix typo.Théo Zimmermann
2019-04-16Update and fix documentation of Program Fixpoint with measureMaxime Dénès
2019-04-10Improve SProp error message to mention the Allow StrictProp flag.Théo Zimmermann
2019-03-30[Manual] TypoVincent Laporte
2019-03-29typo in ring.rstthery
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
2019-03-27Merge PR #9828: Fix syntax of Typeclasses eauto := in reference manual.Jim Fehrle
2019-03-27Deprecate `Refine Instance Mode` optionMaxime Dénès
2019-03-26Fix syntax of Typeclasses eauto := in reference manual.Théo Zimmermann
2019-03-25Remove `Automatic Coercions Import` option.Maxime Dénès
2019-03-18Update doc and changesKazuhiko Sakaguchi
2019-03-18[Manual] Move command Context after Let, and more polishingLysxia
2019-03-17[Manual] Move doc on Let into Section mechanism, and more polishingLysxia
2019-03-17[Manual] Gather section-specific commands in Section documentation (fix #9704)Lysxia
2019-03-17[Manual] Improve chapter Type classes, and add mention of Context under VariableLysxia
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-13[refman] Fix other newly emitted warnings.Théo Zimmermann
2019-02-28[sphinx] Add warn option to coqtop directive.Théo Zimmermann
2019-02-18Using options abort and restart of coqtop directive in the manual.Théo Zimmermann
2019-02-18Fix doc for Refine Instance ModeGaëtan Gilbert
2019-02-18Fix failing coqtops in type-classes.rstGaëtan Gilbert
2019-02-14[Manual] Fix a referenceVincent Laporte
2019-02-13Merge PR #9553: Sphinx various fixing of failing commandsThéo Zimmermann
2019-02-12Fix failing coqtops universe-polymorphism.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ring.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in micromega.rst (the main one requires csdp)Gaëtan Gilbert
2019-02-12Fix failing coqtops in generalized-rewriting.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in extended-pattern-matching.rstGaëtan Gilbert
2019-02-11Small typos in the documentation.Martin Bodin
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
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-22Remove unneeded | in productionlistsJim Fehrle
2018-12-04Add undocumented options from mattam82Jim Fehrle
2018-12-04Document undocumented flags and optionsJim Fehrle
2018-12-03A few fixes of unexisting tokens.Théo Zimmermann
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-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-27[Typeclasses] Warn when RHS of `:>` is not a classVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 16:30:46 +0000