aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2019-09-18Merge PR #9856: A 'zify' tactic as a ML pluginMaxime Dénès
2019-09-17Add changelog entryMaxime Dénès
2019-09-16Re-implementation of zifyFrédéric Besson
2019-09-12Merge PR #10753: Release notes for 8.10+beta3.Clément Pit-Claudel
2019-09-12Release notes for 8.10+beta3.Théo Zimmermann
2019-09-10Refman: To be compatible gtk2/gtk3, not mentioning GTK+ version explicitely.Hugo Herbelin
2019-09-10Fixing coqide doc about location of "coqiderc" and "coqide.bindings".Hugo Herbelin
2019-09-09Merge PR #9379: Vectors: lemmas about uncons and splitAtHugo Herbelin
2019-09-05Merge PR #10731: Ocfnash/stdlib additionsHugo Herbelin
2019-09-05Merge PR #10730: Add missing index for From ... Require ...Clément Pit-Claudel
2019-09-04Add changelog entry for 10731Oliver Nash
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
2019-09-03Add missing index for From ... Require ...Théo Zimmermann
2019-09-03Apply suggestions from code reviewOliver Nash
2019-09-03New lemmas for List.vOliver Nash
2019-09-01edits per reviewYishuai Li
2019-09-01Changelog: more accurate on unconsYishuai Li
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
2019-08-25Merge PR #10632: Prove the completeness of real numbers from logical axiom si...Hugo Herbelin
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
2019-08-23[doc] Fix documentation of schedule-vioEmilio Jesus Gallego Arias
2019-08-20Merge PR #10291: Controlling typing flags with commands (no attribute)Gaëtan Gilbert
2019-08-19Split ConstructiveRealsLUB and improve commentsVincent Semeria
2019-08-16Fix quoting in 8.9 changelog entry.Théo Zimmermann
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-09Add a changelog entryKazuhiko Sakaguchi
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
2019-08-08Add interface of constructive real numbers, with an opaque implementation by ...Vincent Semeria
2019-08-05Merge PR #10624: Remove reference to removed option Printing Primitive Projec...Théo Zimmermann
2019-08-05Merge PR #10608: Copy edit the Ltac2 documentationJim Fehrle
2019-08-05Remove reference to removed option Printing Primitive Projection CompatibilityJim Fehrle
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-07-31Merge PR #9811: [stdlib] Remove deprecated module ZlogarithmEmilio Jesus Gallego Arias
2019-07-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
2019-07-29Document changes by PR 10324Vincent Laporte
2019-07-29Merge PR #10548: Refine documentation of tokensThéo Zimmermann
2019-07-29Merge PR #10574: Remove deprecated `Backtrack` commandEnrico Tassi
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
2019-07-26Remove the tactic wizard, as it has not worked for several years and no one c...Guillaume Melquiond
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
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-20Merge PR #9884: doc_grammar, a utility to extract Coq's grammar from .mlg fil...Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 05:06:24 +0000