aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-04-16Fix spurious argument of {measure}Maxime Dénès
2019-04-16Take advantage of relaxed {measure} syntax in test suiteMaxime Dénès
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
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-11[stm] Report correct ids on some errors where it was dummy.Shachar Itzhaky
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-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-08Fix spelling in comment.nlewycky
2019-04-08Fix #9812: CoqIDE on gtk3 has wrong defaults for selection BG.Pierre-Marie Pédrot
2019-04-08Don't store closures in summary (reduction effects)Gaëtan Gilbert
2019-04-08Merge PR #9915: Remove cache in HeadsEnrico Tassi
2019-04-08Merge PR #9900: [native compiler] Fix critical bug with stuck primitive proje...Pierre-Marie Pédrot
2019-04-06Merge PR #9924: Fix numeral notations test in async mode.Emilio Jesus Gallego Arias
2019-04-06Fix numeral notations test in async mode.Gaëtan Gilbert
2019-04-06Merge PR #9923: [ci/deploy] Fix branch creation when pushing to coq/coq-on-ca...Emilio Jesus Gallego Arias
2019-04-06[ci/deploy] Fix branch creation when pushing to coq/coq-on-cachix.Théo Zimmermann
2019-04-05[native compiler] Fix critical bug with primitive projectionsMaxime Dénès
2019-04-05[native compiler] Normalize before destructuring sortMaxime Dénès
2019-04-05[api] [proofs] Remove dependency of proofs on interp.Emilio Jesus Gallego Arias
2019-04-05Merge PR #9685: [vernac] Small cleanup to remove assert false.Vincent Laporte
2019-04-05Remove cache in HeadsMaxime Dénès
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 10:43:08 +0000