aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2019-12-04[dune] Update to dune language version 2.0Emilio Jesus Gallego Arias
This is the minimal set of changes requires for Coq to build under 2.0 mode. We may likely take advantage of some more new features. Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune in older versions as it will install a secondary compiler.
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-02List of 8.11 contributors and stats.Théo Zimmermann
2019-12-02Merge redundant consecutive changelog entries on reals.Théo Zimmermann
2019-12-02Highlight refine attribute for Instance.Théo Zimmermann
2019-12-02Warn more clearly about incompatibilities coming from #10476.Théo Zimmermann
2019-12-028.11 release notes.Matthieu Sozeau
2019-12-02Move unreleased changelog to new 8.11 section.Théo Zimmermann
2019-12-02Merge PR #10575: Clean up deprecationsThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: silene
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
The manual was already saying that it was deprecated, but no warning was emitted. Fixes #10572
2019-11-30Deprecation annotation for `convert_concl_no_check`Maxime Dénès
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-28Release notes for Coq 8.10.2Vincent Laporte
2019-11-27weaker then -> weaker thanlarsr
2019-11-25Minor fix in doc for [unfold]Gaëtan Gilbert
Close #9634
2019-11-21Merge PR #11145: Document -vos flag for coqdepEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
Ack-by: Zimmi48
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
Reviewed-by: gares Reviewed-by: silene
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed.
2019-11-20Merge PR #11119: 8.10-backportable part of #10575Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing ↵charguer
(fixing bug #11057). With this new behavior, it is not needed to .vos files in user contribs. Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-11-14Merge PR #10979: Fix doc for universes(foo) attributesThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-14Fix doc for universes(foo) attributesGaëtan Gilbert
Fix #10570
2019-11-14Merge PR #11100: small documentation fixesThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2019-11-14doc fixesAntonio Nikishaev
2019-11-14Restore documentation of `Typeclasses Axioms Are Instances`Maxime Dénès
This documentation seems to have been lost after it was introduced by 0ad26633a4589d77de1f864733d1d953dab9ea91 We also document that this flag is deprecated.
2019-11-14Document recommended syntax for `firstorder`Maxime Dénès
Only the deprecated one was documentated, and the deprecation was not mentioned.
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
We can now do `#[refine] Instance : Bla := bli.` to enter proof mode with `bli` as a starting refinement. If `bli` is enough to define the instance we still enter proof mode, keeping things nicely predictable for the stm.
2019-11-08Merge PR #11050: Replace "option" in doc when it refers to a flagThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-11-04Cite POPL19 SProp paperGaëtan Gilbert
Close #10242
2019-11-03Elan → Stratego in documentation of `rewrite_strat`.Robbert Krebbers
@eelcovisser told me that the strategies in Luttik and Visser 97 were inspired by Elan, but they are not part of Elan. They are part of the Stratego language.
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) ↵Enrico Tassi
relation Reviewed-by: gares
2019-11-01Update the deprecation doc of `Shrink Obligations`Jason Gross
Now it uses `.. deprecated` like all the other deprecation notices in the manual.
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes Ack-by: proux01 Ack-by: silene Ack-by: vbgl
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
A .vos file stores the result of compiling statements (defs, lemmas) but not proofs. A .vok file is an empty file that denotes successful compilation of the full contents of a .v file. Unlike a .vio file, a .vos file does not store suspended proofs, so it is more lightweight. It cannot be completed into a .vo file.
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
Ack-by: Zimmi48 Ack-by: cpitclaudel Reviewed-by: ejgallego
2019-10-31Merge PR #9883: Add support for Sorts in numeral notationsVincent Laporte
Ack-by: SkySkimmer Ack-by: proux01 Reviewed-by: vbgl
2019-10-31Merge PR #10997: Implement the unsupported attribute error using the warning ↵Emilio Jesus Gallego Arias
system Reviewed-by: Zimmi48 Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-27 17:09:07 +0000