aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-11Update doc/sphinx/proof-engine/ssreflect-proof-language.rstFlorent Hivert
2019-07-11Merge PR #10439: Uniform handling of side-effects for opaque definitionsMaxime Dénès
2019-07-10Fixed a few wrong reference and typosFlorent Hivert
2019-07-08Adding a changelog.Pierre-Marie Pédrot
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-05Correct doc about default value for Typeclasses Dependency OrderGaëtan Gilbert
2019-07-04Fix miscellaneous mistakes in unreleased changelog entries.Théo Zimmermann
2019-07-03Merge PR #10419: [api] Refactor most of `Decl_kinds`Gaë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-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
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-24[api] Move `locality` from `library` to `vernac`.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
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-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
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 py-style headers to new year.Théo Zimmermann
2019-06-17Update c-style headers to new year.Théo Zimmermann
2019-06-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
2019-06-17Merge PR #10368: Update, expand, and document plugin tutorial 2Enrico Tassi
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-15Merge PR #10377: Rename expr and tacexpr tokens into ltac_expr token family.Clément Pit-Claudel
2019-06-15Rename expr and tacexpr tokens into ltac_expr token family.Théo Zimmermann
2019-06-14Merge PR #10376: Add a comment documenting what fontsupport.py is.Clément Pit-Claudel
2019-06-14Add a comment documenting what fontsupport.py is.Théo Zimmermann
2019-06-14Merge PR #10322: Update changes.rst as a follow-up to #9743Théo Zimmermann
2019-06-13Merge PR #10374: Integrate 8.9.0 and 8.9.1 changelog entries.Clément Pit-Claudel
2019-06-13Integrate 8.9.0 and 8.9.1 changelog entries.Théo Zimmermann
2019-06-13Add missing changelog entry for #10360.Théo Zimmermann
2019-06-13Update, expand, and document plugin tutorial 2Talia Ringer
2019-06-12Merge PR #10310: Fix #10283: clearer dependency documentation for building Co...Clément Pit-Claudel
2019-06-12Merge PR #10329: Update changelog for 10302 and 10305Théo Zimmermann
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-09Merge PR #8726: More robust treatment of the Discharge statusPierre-Marie Pédrot
2019-06-09Merge PR #10245: Command line: adding variants for Require, aligning on the v...Emilio Jesus Gallego Arias
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
2019-06-08Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ...Pierre-Marie Pédrot
2019-06-08Updated changelog.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 06:50:44 +0000