aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-04-16Command-line setters for optionsGaëtan Gilbert
2019-04-16[CI/Azure/macOS] Set MACOSX_DEPLOYMENT_TARGET to 10.12Vincent Laporte
2019-04-16[CI/Azure/macOS] Install Coq into an artifactVincent Laporte
2019-04-15Update critical-bugsPierre Roux
2019-04-15[vm] Protect accu and coq_envPierre Roux
2019-04-15[native compiler] Encoding of constructors based on tagsMaxime Dénès
2019-04-15[native compiler] Remove unused universe argument in LmakeblockMaxime Dénès
2019-04-15[native compiler] Distinguish constant constructors in lambda codeMaxime Dénès
2019-04-15[CI/Azure/macOS] Build CoqIDEVincent Laporte
2019-04-15[CoqIDE] Fix build system for macOSVincent Laporte
2019-04-15[CI] Print test-suite log on failure (macOS/Azure)Vincent Laporte
2019-04-15Merge PR #9927: Don't store closures in summary (reduction effects)Pierre-Marie Pédrot
2019-04-15Merge PR #9959: [native compiler] Remove `Lconstruct` from lambda code.Pierre-Marie Pédrot
2019-04-14[native compiler] Remove now unused GconstructMaxime Dénès
2019-04-14[native compiler] Remove `Lconstruct` from lambda code.Maxime Dénès
2019-04-14Merge PR #9957: Add missing build dependency in `coq.opam`Emilio Jesus Gallego Arias
2019-04-14Fix coq/coq#9956Erik Martin-Dorel
2019-04-12Merge PR #9949: [stm] Report correct ids on some errors where it was dummy.Enrico Tassi
2019-04-12Remove `constr_of_global_in_context`Maxime Dénès
2019-04-12Unify Set and Unset handling for optionsGaëtan Gilbert
2019-04-11[stm] Report correct ids on some errors where it was dummy.Shachar Itzhaky
2019-04-11Merge pull request coq/ltac2#119 from maximedenes/pretyping-rm-globalPierre-Marie Pédrot
2019-04-11Merge PR #9909: Remove all but one call to `Global` in the pretyperPierre-Marie Pédrot
2019-04-11Merge PR #9938: [coqdep] Exit with error code on exception.Pierre-Marie Pédrot
2019-04-10Merge PR #9943: [mailmap] Tweak Emilio's entries.Théo Zimmermann
2019-04-10Merge PR #9910: [api] [proofs] Remove dependency of proofs on interp.Gaëtan Gilbert
2019-04-10Overlays for Global removal in pretyperMaxime Dénès
2019-04-10Remove calls to Global.env in HeadsMaxime Dénès
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-04-10Remove calls to Global.env from EvarsolveMaxime Dénès
2019-04-10Remove calls to Global.env and Libobject from RecordopsMaxime Dénès
2019-04-10Remove calls to Global.env in TypingMaxime Dénès
2019-04-10Remove calls to Global.env in Glob_opsMaxime Dénès
2019-04-10Remove calls to Global.env in PatternopsMaxime Dénès
2019-04-10Remove call to global env in pretyping.mlMaxime Dénès
2019-04-10Functionalize env in type classesMaxime Dénès
2019-04-10Move vernac-related part of coercions to vernacMaxime Dénès
2019-04-10Remove one call to Global.env in DetypingMaxime Dénès
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-04-10Fix constant order in heads.mlMaxime Dénès
2019-04-10[mailmap] Tweak Emilio's entries.Emilio Jesus Gallego Arias
2019-04-10Merge PR #9941: Improve SProp error message to mention the Allow StrictProp f...Gaëtan Gilbert
2019-04-10Improve SProp error message to mention the Allow StrictProp flag.Théo Zimmermann
2019-04-10[coqdep] Exit with error code on exception.Emilio Jesus Gallego Arias
2019-04-09[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.Emilio Jesus Gallego Arias
2019-04-09Merge PR #9928: Fix #9812: CoqIDE on gtk3 has wrong defaults for selection BG.Enrico Tassi
2019-04-09Merge PR #9931: Fix spelling in comment.Théo Zimmermann
2019-04-09Adapt to Coq's PR #9909Maxime Dénès
2019-04-09Add a few missing notes to the release doc.Théo Zimmermann
2019-04-08Fix spelling in comment.nlewycky