aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2019-06-16Changelog for 8.10+beta2.Théo Zimmermann
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-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
2019-06-08Mini fix documentation coqtop in passing.Hugo Herbelin
2019-06-08Documenting new options -require-import, -require-export, etc.Hugo Herbelin
2019-06-07Merge PR #10311: Ltac2 codeowner / changelogMaxime Dénès
2019-06-07Update changelog for 103032 and 10305Enrico Tassi
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06Update changes.rst as a follow-up to #9743Kazuhiko Sakaguchi
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
2019-06-06Clean, document, and expand plugin tutorials 0 and 1Talia Ringer
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-05Changelog entry for Ltac2 (missing from #10002).Théo Zimmermann
2019-06-05Fix #10283: clearer dependency documentation for building CoqIDE.Théo Zimmermann
2019-06-04Fix typo in changelogEnrico Tassi
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-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-06-03Merge PR #10287: Update tutorial plugin to use sigma instad of evd, in keepin...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 tutorial plugin to use sigma, in keeping with doc recommendationsTalia Ringer
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-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 11:05:25 +0000