aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-05-06Mention keywords from g_ltac.mlg used in Ltac.Hugo Herbelin
2020-05-06Mention keywords used in tactics from g_tactic.mlg.Hugo Herbelin
2020-05-06Documenting plugin/tactic/stdlib keywords in corresponding chapters.Hugo Herbelin
Incidentally removing "discriminated", "(bfs)" and "(dfs)" from keywords. It is enough to make them normal identifiers. Note: - keywords reserved by the tactics are: ** [= _eqn |- by using - keywords reserved by ltac are: lazymatch multimatch ||
2020-05-05[refman] Add missing (only parsing) to example of compat notations.Théo Zimmermann
2020-05-04Merge PR #12211: When TIMED=1, emit timing info for OCaml filesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-03Merge PR #12197: LtacProf now handles multi-success backtrackingPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
Fixes #12196
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-05-01Preserve vernac chapter.Théo Zimmermann
2020-05-01Extract two new files out of Gallina chapter.Théo Zimmermann
2020-05-01Create section on writing libraries with only deprecated attributes.Théo Zimmermann
2020-05-01Extract deprecated attribute from Gallina chapter.Théo Zimmermann
2020-05-01Remove flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Remove lexical conventions and attributes from Gallina chapter.Théo Zimmermann
2020-05-01Create basics out of sections from Gallina and Vernac chapters.Théo Zimmermann
2020-05-01Create section on basics with just flags, options and tables.Théo Zimmermann
2020-05-01Extract flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Create section on basics with just lexical conventions and attributes.Théo Zimmermann
2020-05-01Extract lexical conventions and attributes from Gallina chapter.Théo Zimmermann
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:26:28 +0000