aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-08-29Merge PR #9066: [parsing] Move pcoq-specific parts in extend to pcoq.Pierre-Marie Pédrot
2019-08-29Merge PR #10703: Make Bool.eqb_spec transparentHugo Herbelin
2019-08-29Merge PR #10643: [glob/aux files] Remove undocumented Stdout dump, cleanup fl...Hugo Herbelin
2019-08-29Fix a few wrong uses of `msg_notice`Maxime Dénès
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-29Remove wrong advice to base feedback level choice on encoding issuesMaxime Dénès
2019-08-29Logic monad debug printer now emits a debug messageMaxime Dénès
2019-08-28Merge PR #10488: Simplify picking between uint63_63.ml and uint63_31.ml + mak...Enrico Tassi
2019-08-28Merge PR #10646: Recommend assigning an issue before fixing a bug.Emilio Jesus Gallego Arias
2019-08-28Merge PR #10709: Add missing entry to the contributing guide TOC.Emilio Jesus Gallego Arias
2019-08-27[ci] Update to OCaml 4.08.1Emilio Jesus Gallego Arias
2019-08-27[declare] Use entry constructor instead of low-level record.Emilio Jesus Gallego Arias
2019-08-27Merge PR #10680: Tauto: use Coqlib to locate “not” and “NNPP”Pierre-Marie Pédrot
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-08-27[cleanup] Replace uses of UserError constructor, clarify exception names.Emilio Jesus Gallego Arias
2019-08-27Merge PR #10635: [funind] Port indfun to the new tactic engine.Pierre-Marie Pédrot
2019-08-27Add missing entry to the contributing guide TOC.Théo Zimmermann
2019-08-26Test-suite fixes from HugoMatthieu Sozeau
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-26Tauto: use Coqlib to locate “not” and “NNPP”Vincent Laporte
2019-08-26Merge PR #10677: coqchk: Cleanup environment manipulation in check_constant_d...Pierre-Marie Pédrot
2019-08-26Merge PR #10696: [lib] [future] Small cleanup of ununsed functions.Pierre-Marie Pédrot
2019-08-26[glob/aux files] Remove undocumented Stdout dump, cleanup flags.Emilio Jesus Gallego Arias
2019-08-26[lib] [future] Small cleanup of ununsed functions.Emilio Jesus Gallego Arias
2019-08-25Make Bool.eqb_spec transparentTej Chajed
2019-08-25Changed chmod -w to chmod a-w to avoid error on cygwinMichael Soegtrop
2019-08-25Merge PR #10632: Prove the completeness of real numbers from logical axiom si...Hugo Herbelin
2019-08-24saner cond_flags in makefileGaëtan Gilbert
2019-08-24Simplify picking between uint63_63.ml and uint63_31.mlGaëtan Gilbert
2019-08-24[gitlab/ci] Prevent Corn from running if Bignums has failed.Théo Zimmermann
2019-08-24Merge PR #10698: [dune] Migrate static Dune files to Dune 1.10Théo Zimmermann
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
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