aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2019-07-23doc: Fix a detail in 2 files describing the under tacticErik Martin-Dorel
2019-07-22[Int63] Implement all primitives in OCamlVincent Laporte
2019-07-22[Extraction] Add support for primitive integersVincent Laporte
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-11Merge PR #10424: Update doc for % escapes in Sphinx, improve error messagesClément Pit-Claudel
2019-07-11Update doc/sphinx/proof-engine/ssreflect-proof-language.rstFlorent Hivert
2019-07-10Fixed a few wrong reference and typosFlorent Hivert
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-07-01Update doc for % escapes in Sphinx doc, improve error messagesJim Fehrle
2019-06-30Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.Emilio Jesus Gallego Arias
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
2019-06-25Give a functional type to Ltac1 quotations with a context.Pierre-Marie Pédrot
2019-06-25Documenting the Ltac2 change.Pierre-Marie Pédrot
2019-06-19Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations i...Théo Zimmermann
2019-06-17Merge PR #10392: Fix the changelog of 8.10+beta2 following the backport of #1...Clément Pit-Claudel
2019-06-17Fix the changelog of 8.10+beta2 following the backport of #10205.Théo Zimmermann
2019-06-17Update copyright years outside of headers.Théo Zimmermann
2019-06-17Adapt change-header script to handle shebangs in addition to Emacs comments.Théo Zimmermann
2019-06-17Update c-style headers to new year.Théo Zimmermann
2019-06-16Changelog for 8.10+beta2.Théo Zimmermann
2019-06-16Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".Hugo Herbelin
2019-06-15Rename expr and tacexpr tokens into ltac_expr token family.Théo Zimmermann
2019-06-14Merge PR #10322: Update changes.rst as a follow-up to #9743Théo Zimmermann
2019-06-13Integrate 8.9.0 and 8.9.1 changelog entries.Théo Zimmermann
2019-06-12Merge PR #10310: Fix #10283: clearer dependency documentation for building Co...Clément Pit-Claudel
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-09Merge PR #10245: Command line: adding variants for Require, aligning on the v...Emilio Jesus Gallego Arias
2019-06-08Mini fix documentation coqtop in passing.Hugo Herbelin
2019-06-08Documenting new options -require-import, -require-export, etc.Hugo Herbelin
2019-06-06Update changes.rst as a follow-up to #9743Kazuhiko Sakaguchi
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-06-05Fix #10283: clearer dependency documentation for building CoqIDE.Théo Zimmermann
2019-06-04[rewrite] Add Morphism syntax made different for module type parametersEnrico Tassi
2019-06-04[function] always open a proof when used with `wf` or `measure`Enrico Tassi
2019-06-03Merge PR #10277: Remove Show Script (deprecated in 8.10)Théo Zimmermann
2019-06-03Merge PR #10261: Update doc to reflect that PG now supports Coq-generated pro...Théo Zimmermann
2019-06-03Update doc to reflect that PG now supports Coq-generated proof diffsJim Fehrle
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-26Merge PR #10220: Use new coqrst syntax for alternatives in SSReflect chapter.Enrico Tassi
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
2019-05-23Merge PR #10118: Make progress toward #9411: reject new undefined references.Clément Pit-Claudel
2019-05-24Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}`Emilio Jesus Gallego Arias
2019-05-23Make progress toward #9411: reject new undefined references.Théo Zimmermann
2019-05-23Merge PR #10195: Minor Ltac2 documentation fix: type parameters are optional.Clément Pit-Claudel
2019-05-23Merge PR #10217: Less undefined tokensClément Pit-Claudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 13:05:46 +0000