aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-08coq_makefile install target: error if any file is missingGaëtan Gilbert
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-06Fix pretty-printing of primitive integersErik Martin-Dorel
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 pull request coq/ltac2#116 from proux01/master-parsing-decimalPierre-Marie Pédrot
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-02-10 03:41:21 +0000