aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum
AgeCommit message (Expand)Author
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
2019-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ...Pierre-Marie Pédrot
2019-10-04Allow SProp default onGaëtan Gilbert
2019-10-03Improved handling of micromega cachesFrédéric Besson
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
2019-09-25Adding documentation for the move of sections data to kernel.Pierre-Marie Pédrot
2019-09-16Re-implementation of zifyFrédéric Besson
2019-08-23[doc] Fix documentation of schedule-vioEmilio Jesus Gallego Arias
2019-07-22Merge PR #10441: Attach the universe polymorphic status to sections.Gaëtan Gilbert
2019-07-18[doc] Fix typo in doc/sphinx/addendum/ring.rstWojciech Nawrocki
2019-07-18Adding changelog and documentation.Pierre-Marie Pédrot
2019-07-05Correct doc about default value for Typeclasses Dependency OrderGaëtan Gilbert
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ...Kazuhiko Sakaguchi
2019-06-04[rewrite] Add Morphism syntax made different for module type parametersEnrico Tassi
2019-05-24Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}`Emilio Jesus Gallego Arias
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
2019-05-22[refman] Add more missing @ signsClément Pit-Claudel
2019-05-21Fixing typos - Part 1JPR
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-19[refman] Fix up the documentation of Instance and Existing InstanceClément Pit-Claudel
2019-05-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clément Pit-Claudel
2019-05-19Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual ...Théo Zimmermann
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 20:42:51 +0000