aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-04-30[zify] add support for Nat.le, Nat.lt and Nat.eqFrédéric Besson
Nat.le, Nat.lt and Nat.eq are aliased to le, lt and @eq nat. The required declarations are now added in ZifyInst.
2020-04-30do not re-export ListNotations from Program: changelogAntonio Nikishaev
2020-04-29When TIMED=1, emit timing info for OCaml filesJason Gross
2020-04-29Merge PR #11606: [tools] Add memory stats to tables by defaultEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-29Merge PR #12027: Fix #3415: coqdoc links projections rather than constructor ↵Emilio Jesus Gallego Arias
in record tuples Reviewed-by: ejgallego
2020-04-29Merge PR #12150: Support in-line glossary definitions and references with an ↵Clément Pit-Claudel
index Ack-by: Zimmi48
2020-04-29Merge PR #12195: [doc] [sphinx] Run in silent mode by defaultThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-29Support in-line glossary entries and referencesJim Fehrle
with an index
2020-04-28[doc] [sphinx] Be silent when running latexmkEmilio Jesus Gallego Arias
This is actually supported by Sphinx directly.
2020-04-28[doc] [sphinx] Run in silent mode by defaultEmilio Jesus Gallego Arias
The convention in the dune build is to be silent except for warnings and errors, so they don't go unnoticed. We could have this controlled by a variable if needed (likely would require some support from Dune?) Solves part of #12194
2020-04-28Merge PR #12183: Suggestion of improvement for the Allow SProp error message.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: jfehrle
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-27Merge PR #12073: Split off Nsatz tactic part into Nsatz_tacticPierre-Marie Pédrot
Reviewed-by: anton-trunov Reviewed-by: ppedrot
2020-04-27Merge PR #12168: [dune] Fix dependencies of refman.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-27Merge PR #12090: Remove documentation for Hide menu in CoqIDE (was removed ↵Clément Pit-Claudel
in 8.5).
2020-04-27Merge PR #12132: [refman] Remove references to omega from Tactics chapter.Vincent Laporte
Reviewed-by: vbgl
2020-04-27Further documentation improvements.Théo Zimmermann
2020-04-27Improve the Allow SProp error message.Théo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-26Merge PR #12176: Doc: extend example for induction a bitThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-25Doc: extend example for induction a bitGaëtan Gilbert
This makes it show the shape of the induction hypothesis in the second goal instead of just saying "subgoal 2 is S n <= S n".
2020-04-25Merge PR #12173: CoqIDE: Revert overzealous application of language-based ↵Pierre-Marie Pédrot
highlighting from #12169 Reviewed-by: ppedrot
2020-04-24[nsatz] Use Export rather than IncludeJason Gross
As per https://github.com/coq/coq/pull/12073#issuecomment-612869336
2020-04-24Add memory stats to tables by defaultJason Gross
The Python scripts now support `--no-include-mem` to turn it off, and also support `--sort-by-mem`. Closes #11575
2020-04-24Split off Nsatz tactic part into NsatzTacticJason Gross
Closes #5445 Note that we use `Include` rather than `Export` to expose the machinery defined in `NsatzTactic` from `Nsatz` to preserve backwards compatibility with developments relying on absolute names of the constants previously defined in `Nsatz.v`.
2020-04-24CoqIDE: Revert overzealous application of language-based highlighting in #12169.Hugo Herbelin
The parsing rules defining classes of lexemes in language configuration expect a Coq document and are not relevant in the message and proof window. Thus backtracking on this part of #12169. Keeping the highlighting style though.
2020-04-24[dune] Fix dependencies of refman.Théo Zimmermann
Dependencies specified through an alias do not trigger a rebuild when they are modified. This is likely a Dune bug, but we still need to fix this on our side as this is inconvenient.
2020-04-24Merge PR #12156: Document `+` in polymorphic universe levelsThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-23Merge PR #12154: [documentation] ssreflect: Abbreviations do not support scopeThéo Zimmermann
Ack-by: Zimmi48 Reviewed-by: gares
2020-04-23Merge PR #12117: Make multiplication of Cauchy reals transparent and ↵Hugo Herbelin
accelerate it Reviewed-by: herbelin
2020-04-23Merge PR #12120: Fixing #12119 : remove useless hypothesis in ↵Hugo Herbelin
NoDup_Permutation_bis Reviewed-by: herbelin
2020-04-23[documentation] ssreflect: Abbreviations do not support scopeKenji Maillard
2020-04-23Merge PR #12148: Consolidate funind documentation onto a single page.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-04-23[refman] Fix name of tactic: function induction -> functional induction.Théo Zimmermann
2020-04-23Fix coq snippets in Tactics chapter.Théo Zimmermann
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command ↵Pierre-Marie Pédrot
line -sprop-cumulative Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-04-22Merge PR #11928: Remove probably useless doc/sphinx/coqdoc.css.Hugo Herbelin
2020-04-22Merge PR #12031: [stdlib] A library on cyclic permutations: CPermutationHugo Herbelin
Ack-by: Zimmi48 Ack-by: anton-trunov Reviewed-by: herbelin
2020-04-22Document Cauchy realsVincent Semeria
2020-04-22Merge PR #12023: Adding a Declare ML Module in empty file Ltac.vEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: ppedrot
2020-04-22Document `+` in polymorphic universe levelsKenji Maillard
2020-04-21Change log for #12023Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-04-21Adding a Declare ML Module in empty file Ltac.v.Hugo Herbelin
Indeed, it would be intuitive that `Require Import Ltac` is an equivalent for Ltac of `Require Import Ltac2.Ltac2`. Also declaring the classic proof mode.
2020-04-21Change log.Hugo Herbelin
2020-04-21Document changed warnings and erros following #12038.Théo Zimmermann
2020-04-21Update common.edit_mlg and fullGrammar following #12038.Théo Zimmermann
2020-04-21Move documentation on Funind into a single file.Théo Zimmermann
2020-04-21Merge all documentation on Funind into the same file.Théo Zimmermann
2020-04-21Consolidate funind tactics and Functional Scheme in Funind section of the ↵Théo Zimmermann
Libraries chapter.
2020-04-21Extract funind tactics to funind section of the Libraries chapter.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 13:29:51 +0000