aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2019-11-25Minor fix in doc for [unfold]Gaëtan Gilbert
2019-11-21Merge PR #11145: Document -vos flag for coqdepEmilio Jesus Gallego Arias
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
2019-11-21Document -vos flag for coqdepGaëtan Gilbert
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-11-20Merge PR #11119: 8.10-backportable part of #10575Clément Pit-Claudel
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixin...charguer
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
2019-11-14Merge PR #10979: Fix doc for universes(foo) attributesThéo Zimmermann
2019-11-14Fix doc for universes(foo) attributesGaëtan Gilbert
2019-11-14Merge PR #11100: small documentation fixesThéo Zimmermann
2019-11-14doc fixesAntonio Nikishaev
2019-11-14Restore documentation of `Typeclasses Axioms Are Instances`Maxime Dénès
2019-11-14Document recommended syntax for `firstorder`Maxime Dénès
2019-11-13Return of Refine Instance as an attribute.Gaë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-11-03Elan → Stratego in documentation of `rewrite_strat`.Robbert Krebbers
2019-11-01Merge PR #11028: Update the deprecation doc of `Shrink Obligations`Clément Pit-Claudel
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...Enrico Tassi
2019-11-01Update the deprecation doc of `Shrink Obligations`Jason Gross
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
2019-11-01Add warnings regarding the experimental nature of the vos feature in the doc.Pierre-Marie Pédrot
2019-11-01fix coq_makefile and doc for vos support.charguer
2019-11-01additional details in the doc for -voscharguer
2019-11-01Implementing support for vos/vok files.charguer
2019-11-01docs(gallina-extensions.rst): Say more on float literals extractionErik Martin-Dorel
2019-11-01docs: Add refman+stdlib documentationErik Martin-Dorel
2019-11-01[ssr] Update doc for under w.r.t. setoid-like relationsErik Martin-Dorel
2019-10-31Merge PR #10985: Print argument info as an Arguments command in AboutEmilio Jesus Gallego Arias
2019-10-31Merge PR #9883: Add support for Sorts in numeral notationsVincent Laporte
2019-10-31Merge PR #10997: Implement the unsupported attribute error using the warning ...Emilio Jesus Gallego Arias
2019-10-31Doc: index command Arguments with assertGaëtan Gilbert
2019-10-31Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.Gaëtan Gilbert
2019-10-30Implement the unsupported attribute error using the warning systemGaë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-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
2019-10-29Show diffs in "Show Proof."Jim Fehrle
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-10-29Document the ability to bind notation arguments in Ltac2.Pierre-Marie Pédrot
2019-10-28Add support for Sorts in numeral notationsJason Gross
2019-10-24Release notes for Coq 8.10.1Vincent Laporte
2019-10-23Better wording for "Show Proof" and fix typosJim Fehrle
2019-10-23Merge PR #10929: documentation fixesThéo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 20:10:51 +0000