aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-08-23[lemmas] Cleanup users of default proof information.Emilio Jesus Gallego Arias
2019-08-23coqchk: Cleanup environment manipulation in check_constant_declarationGaëtan Gilbert
2019-08-23Merge PR #10686: DAG-style pipelinesGaëtan Gilbert
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
2019-08-23[gitlab/ci] Rework stages, always use needs keyword.Théo Zimmermann
2019-08-23Merge PR #10691: [doc] Fix documentation of schedule-vioThéo Zimmermann
2019-08-23Create a maintainer team for the contributing process files.Théo Zimmermann
2019-08-23[doc] Fix documentation of schedule-vioEmilio Jesus Gallego Arias
2019-08-22[gitlab/ci] Do not wait for all builds to finish to run the tests.Théo Zimmermann
2019-08-22[gitlab/ci] Build Bignums only once.Théo Zimmermann
2019-08-22[gitlab/ci] Deploy sooner thanks to new needs keyword.Théo Zimmermann
2019-08-22Merge PR #10515: [dune] Move to Dune 1.10, use coq.pp directive.Théo Zimmermann
2019-08-22Merge PR #9062: Delay the computation of frozen evars in legacy unification.Matthieu Sozeau
2019-08-22[dune] Move to Dune 1.10, use coq.pp directive.Emilio Jesus Gallego Arias
2019-08-21Merge PR #10678: [ci] Remove dead code.Emilio Jesus Gallego Arias
2019-08-21Merge PR #10666: [api] Move `Keys` to pretypingEnrico Tassi
2019-08-20[ci] Remove dead code.Théo Zimmermann
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-19Merge PR #10672: Std++, Iris, and Lambda-Rust have moved.Emilio Jesus Gallego Arias
2019-08-19Merge PR #10671: Remove links to doc artifacts and replace them with the depl...Emilio Jesus Gallego Arias
2019-08-19[declare] Use `binding_kind` for implicit kind instead of boolean.Emilio Jesus Gallego Arias
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-08-19Remove links to doc artifacts and replace them with the deployed versions.Théo Zimmermann
2019-08-19Std++, Iris, and Lambda-Rust have moved.Théo Zimmermann
2019-08-19Merge PR #10454: [vernac] Refactor control attributes and fix bug #10452Gaëtan Gilbert
2019-08-19[pcoq] Remove unneeded casting operators.Emilio Jesus Gallego Arias
2019-08-19[parsing] Move pcoq-specific parts in extend to pcoq.Emilio Jesus Gallego Arias
2019-08-18[api] Move `Keys` to pretypingEmilio Jesus Gallego Arias
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
2019-08-16Merge PR #10663: Fix quoting in 8.9 changelog entry.Clément Pit-Claudel
2019-08-16Fix quoting in 8.9 changelog entry.Théo Zimmermann
2019-08-16Fix typing_flags in the checkerSimonBoulier
2019-08-16Fix Print Assumptions: Inductive types can have unsafe fixpoints orSimonBoulier
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-16Add a file for typing_flags in the test-suite.SimonBoulier
2019-08-16Improve [Print Assumptions] for type-in-type and assumed positive.SimonBoulier
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-08-16Add [Print Typing Flags] command.SimonBoulier
2019-08-16Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...SimonBoulier
2019-08-16Apply suggestions from code reviewOliver Nash
2019-08-16New lemmas for List.vOliver Nash
2019-08-16Merge PR #10457: Make rewrite use the registered elimination schemesPierre-Marie Pédrot
2019-08-14[vernac] Refactor common parts of interp_{,delayed}Emilio Jesus Gallego Arias
2019-08-14[vernac] Pass control attributes to interpretation of delayed proofs.Emilio Jesus Gallego Arias
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
2019-08-14Merge PR #10642: Emit Feedback.AddedAxiom in Declare instead of higher layersPierre-Marie Pédrot
2019-08-10[extraction] Fix #7191: Avoid unsound eta-reductionKazuhiko Sakaguchi
2019-08-10Compute (if linear_order_T 0 (IPR 22) (IPR 10) (IPR_pos 10) then true else fa...Vincent Semeria
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 05:38:46 +0000