aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-07-16Removed patch for Gappa tool (verified that changes in gappa master fixed the...Michael Soegtrop
2019-07-16Define constructive real numbers as Cauchy sequences of rational numbers. Red...Vincent Semeria
2019-07-16Enable Coquelicot, Flocq, Interval and Gappa in extended/release Windows buildsMichael Soegtrop
2019-07-16Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and Gappa)Michael Soegtrop
2019-07-16Move unfold_side_flags CClosure -> Tacred internalsGaëtan Gilbert
2019-07-16Merge PR #10520: Fix typosThéo Zimmermann
2019-07-15TyposJim Fehrle
2019-07-15[funind] Remove unneeded callback.Emilio Jesus Gallego Arias
2019-07-15Merge PR #10517: Azure CI MacOS: build byte target firstEmilio Jesus Gallego Arias
2019-07-15Azure CI MacOS: build byte target firstGaëtan Gilbert
2019-07-15Merge PR #10512: Remove Stm.call_process_error_oncePierre-Marie Pédrot
2019-07-14Merge PR #10496: [proof] Minor cleanup in proof.mlPierre-Marie Pédrot
2019-07-11Merge PR #10424: Update doc for % escapes in Sphinx, improve error messagesClément Pit-Claudel
2019-07-11[proof] Minor cleanup in proof.mlEmilio Jesus Gallego Arias
2019-07-11Merge PR #10510: Fixed a few wrong reference and typosThéo Zimmermann
2019-07-11Remove Stm.call_process_error_onceGaëtan Gilbert
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-11Refactor the part about contributing to the stdlib.Théo Zimmermann
2019-07-11More positive wording of the foreword to the contributing guide.Théo Zimmermann
2019-07-11Improve contributing guide further following reviewers' comments.Théo Zimmermann
2019-07-11Refactor and expand contributing guide.Théo Zimmermann
2019-07-11Update doc/sphinx/proof-engine/ssreflect-proof-language.rstFlorent Hivert
2019-07-11Merge PR #10439: Uniform handling of side-effects for opaque definitionsMaxime Dénès
2019-07-10Fixed a few wrong reference and typosFlorent Hivert
2019-07-10Merge PR #10506: merge-pr.sh: filter reviews to remove the PR authorThéo Zimmermann
2019-07-10Merge PR #10509: [CI/Azure/macOS] Attempt at pinning the homebrew-core repos...Emilio Jesus Gallego Arias
2019-07-10[CI/Azure/macOS] Pin the homebrew-core repositoryVincent Laporte
2019-07-10Merge PR #10446: [proof] Remove sign parameter to open_lemma.Gaëtan Gilbert
2019-07-09merge-pr.sh: filter reviews to remove the PR authorGaëtan Gilbert
2019-07-09Merge PR #10471: [core] [api] Support OCaml 4.08Gaëtan Gilbert
2019-07-09[proof] Remove sign parameter to open_lemma.Emilio Jesus Gallego Arias
2019-07-09Merge PR #10453: [errors] Small cleanups and removal of dead code.Gaëtan Gilbert
2019-07-09Merge PR #10067: Faster renaming of shadowed variables in evar instance creat...Hugo Herbelin
2019-07-08Adding a changelog.Pierre-Marie Pédrot
2019-07-08Similar purity invariants in the kernel.Pierre-Marie Pédrot
2019-07-08Further cleanup following the removal of pure opaque definitions.Pierre-Marie Pédrot
2019-07-08Do not export side-effects of polymorphic definitions.Pierre-Marie Pédrot
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-08Merge PR #10497: [lemmas] Move mutually recursive lemma analysis to its own m...Gaëtan Gilbert
2019-07-08[errors] Small cleanups and removal of dead code.Emilio Jesus Gallego Arias
2019-07-08Merge PR #9686: [error] Remove special error printing pre-processingGaëtan Gilbert
2019-07-08Merge PR #10466: [python] Remove use of generic python shebang, update CIGaëtan Gilbert
2019-07-08Merge PR #10246: Investigations in the initialization of coq binaries and com...Emilio Jesus Gallego Arias
2019-07-08Usage: bypassing a useless detour via a reference.Hugo Herbelin
2019-07-08An even more uniform treatment of the -help option across executables.Hugo Herbelin
2019-07-08Removing -filterops "hack" from coqtop.Hugo Herbelin
2019-07-08Some common points between coqc and other coq binaries.Hugo Herbelin
2019-07-08Passing command-line option async_proofs_worker_priority functionally.Hugo Herbelin
2019-07-08Layout/documentation updates.Hugo Herbelin