aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-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-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-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
2019-04-04Update CHANGES.mdPierre Roux
2019-04-04Merge PR #9904: [CI] Fix build of math-comp dependenciesGaëtan Gilbert
2019-04-04[CI] Fix build of math-comp dependenciesMaxime Dénès
2019-04-04Merge PR #9901: [dune] Fix include object dirs.Théo Zimmermann
2019-04-04[dune] Fix include object dirs.Emilio Jesus Gallego Arias
2019-04-04Merge PR #9881: Protect some I/O routines from SIGALRMEmilio Jesus Gallego Arias
2019-04-03Merge PR #9890: Improve coqchk -norec perf by not checking for ill-formed dat...Pierre-Marie Pédrot
2019-04-03Merge PR #9804: CI: Use job-local timeout for build-template and test-suite-t...Emilio Jesus Gallego Arias
2019-04-03Merge PR #9861: [program] Allow evars in type of fixpoints.Gaëtan Gilbert
2019-04-03Protect some I/O routines from SIGALRMMaxime Dénès
2019-04-03Merge PR #9078: Provide a faster bound name generation algorithm through a flagVincent Laporte
2019-04-03Merge PR #9896: Minor correction to numeral notations docThéo Zimmermann
2019-04-03Merge PR #8638: Remove -compat 8.7Théo Zimmermann
2019-04-03Minor correction to numeral notations docJason Gross
2019-04-02Merge PR #9668: Consolidate credits and changelog information in a single place.Clément Pit-Claudel
2019-04-02CI: Use job-local timeout for build-template and test-suite-templateGaëtan Gilbert
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
2019-04-02coqchk: use unsafe marshal for dependencies of -norec librariesGaëtan Gilbert
2019-04-02coqchk: don't marshal opaques for dependencies of -norec librariesGaëtan Gilbert
2019-04-02coqchk: do not validate dependencies of -norec librariesGaëtan Gilbert
2019-04-02Remove -compat 8.7Jason Gross
2019-04-02Merge PR #9875: [doc] Add a note about Dune support to the manual.Théo Zimmermann
2019-04-02Merge PR #9659: Fix #9652: rewrite fails to detect lack of progressEmilio Jesus Gallego Arias
2019-04-02Document the Fast Name Printing option.Pierre-Marie Pédrot
2019-04-02Fast name generation in detyping.Pierre-Marie Pédrot
2019-04-02Define an efficient representation of subscripted identifiers.Pierre-Marie Pédrot
2019-04-02Abstract away the name generation algorithm in Detyping.Pierre-Marie Pédrot
2019-04-02Pass flags through a record in Detyping.Pierre-Marie Pédrot
2019-04-02Add overlaysPierre Roux