aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2019-10-24Release notes for Coq 8.10.1Vincent Laporte
2019-10-23Better wording for "Show Proof" and fix typosJim Fehrle
2019-10-23Merge PR #10932: Add a notation for the empty type.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: amahboubi
2019-10-23Merge PR #10929: documentation fixesThéo Zimmermann
Ack-by: Zimmi48 Reviewed-by: jfehrle
2019-10-22documentation fixesAntonio Nikishaev
document « Property » more documentation fixes [doc] destructed → destructured [doc] another le_minus→lt_1_r [doc] @jfehrle suggestions [doc] more minor fixes
2019-10-22Merge PR #10880: Allow to pass Ltac1 values to Ltac2 quotations.Jason Gross
Ack-by: SkySkimmer Reviewed-by: Zimmi48
2019-10-22Update doc/changelog/06-ssreflect/10932-void-type-ssr.rst Arthur Azevedo de Amorim
Improve changelog. Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-10-22Update changelog.Arthur Azevedo de Amorim
2019-10-22Merge PR #10899: Fixes #10894 regression: uconstr was not anymore typed in ↵Pierre-Marie Pédrot
the Ltac-substituted environment Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-21Improvements of zifyFrédéric Besson
- Fix reification of overloaded operators (triggers convertibility checks with existing terms) - Zify instances need not be in hnf - Fix specification of bool operators - Add (limited) support for comparison fixes #10779
2019-10-21Adding changelogHugo Herbelin
2019-10-18Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in ↵Gaëtan Gilbert
the kernel. Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares
2019-10-18Merge PR #10895: Logic: Add equivalence between weak excluded-middle and ↵Pierre-Marie Pédrot
classical De Morgan's law Reviewed-by: ppedrot
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
This is the dual of #10344.
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
Opening up a lambda should always lift the substitution attached to it.
2019-10-16Define sphinx replacements for \SProp \Type etcGaëtan Gilbert
2019-10-15Merge PR #10854: Fix alphabetical ordering in contributors to 8.10.0.Clément Pit-Claudel
Ack-by: cpitclaudel Reviewed-by: jfehrle
2019-10-15Merge PR #10882: Document Gaëtan's new script to prefill a changelog entry.Clément Pit-Claudel
Ack-by: SkySkimmer Reviewed-by: cpitclaudel
2019-10-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
Reviewed-by: JasonGross Reviewed-by: gares Ack-by: ppedrot
2019-10-14Updating changelogHugo Herbelin
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-13Doc update with mlg extension - fix #10855mcaci
2019-10-11Merge PR #10489: Fix output for "Printing Dependent Evars Line"Hugo Herbelin
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: hendriktews Reviewed-by: herbelin Ack-by: mattam82
2019-10-11Document Gaëtan's new script to prefill a changelog entry.Théo Zimmermann
2019-10-09Fix alphabetical ordering in the list of contributors to 8.10.Théo Zimmermann
Also remove Pierre Letouzey from the list because his contribution was the numeral notation feature which ended up being backported to 8.9, after the branching, but before the first beta release.
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-10-06Merge PR #10834: Fix #10831: minor issues in documentation of Function.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-10-06Fix #10831: minor issues in documentation of Function.Théo Zimmermann
2019-10-068.10.0 release notes.Théo Zimmermann
2019-10-05Changelog for SProp onGaëtan Gilbert
2019-10-05Merge PR #10763: Fix syntax of reduction tactics when listing qualid to ↵Vincent Laporte
reduce or not. Reviewed-by: jfehrle
2019-10-04Improve language.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2019-10-04Merge PR #9772: [Stdlib] OrderedType: do not pollute the “core” hint ↵Pierre-Marie Pédrot
database Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ↵Pierre-Marie Pédrot
sections Reviewed-by: ppedrot
2019-10-04Allow SProp default onGaëtan Gilbert
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-10-04Merge PR #10806: Micromega tactics are no longer confused by primitive ↵Frédéric Besson
projections Reviewed-by: fajb
2019-10-03fix 10765-micromega-caches.rstFrédéric Besson
2019-10-03Improved handling of micromega cachesFrédéric Besson
- Specialised hash and equality functions. Avoid collisions in extreme scenarios. - Flags to disable the use of the caches. fixes #10772
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
We disallow adding univ constraints wich refer to polymorphic universes, and monomorphic constants and inductives when polymorphic universes or constraints are present. Every other combination is already correctly discharged by the kernel.
2019-10-01[Micromega] Use EConstr.eq_constr_universes_projVincent Laporte
2019-09-26Merge PR #10664: Putting sections libstack inside the kernelMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Reviewed-by: maximedenes
2019-09-25Adding documentation for the move of sections data to kernel.Pierre-Marie Pédrot
2019-09-25Merge PR #10713: Define morphisms of real numbers and accelerate Cauchy realsHugo Herbelin
Reviewed-by: herbelin
2019-09-24Merge PR #10774: Make `zify` does work for `Z.to_N`Frédéric Besson
Reviewed-by: Zimmi48 Reviewed-by: fajb
2019-09-24Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopesMatthieu Sozeau
Reviewed-by: mattam82
2019-09-24Make `zify` does work for `Z.to_N`Kazuhiko Sakaguchi
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-09-18Fix syntax of reduction tactics when listing qualid to reduce or not.Théo Zimmermann
2019-09-18Merge PR #9856: A 'zify' tactic as a ML pluginMaxime Dénès
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot Ack-by: vbgl
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:56:14 +0000