aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-03-06Inline the refold and tactic_mode flags for the cbn tactic.Pierre-Marie Pédrot
2021-03-06Merge PR #13586: Support nested timeoutsPierre-Marie Pédrot
2021-03-06Merge PR #13882: Fix #12011 ssreflect "rewrite in" with setoidsPierre-Marie Pédrot
2021-03-06Merge PR #13236: Add a type of format strings to Ltac2.Michael Soegtrop
2021-03-06Merge PR #13902: [coercion] expose coercion_infoPierre-Marie Pédrot
2021-03-06Merge PR #13899: Add noncritical constraint to exception catching in solve_co...Pierre-Marie Pédrot
2021-03-05Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)Pierre-Marie Pédrot
2021-03-05[coercipn] expose coercion_infoEnrico Tassi
2021-03-05Merge PR #13900: doc: don't count a contributor twice in the changelogcoqbot-app[bot]
2021-03-04doc: don't count a contributor twice in the changelogLi-yao Xia
2021-03-04Merge PR #13897: Cleanup internal hint locality handlingcoqbot-app[bot]
2021-03-04Add noncritical constraint to exception catching in solve_constraintsLasse Blaauwbroek
2021-03-04Properly support nested timeoutsLasse Blaauwbroek
2021-03-04Cleanup internal hint locality handlingGaëtan Gilbert
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
2021-03-03Merge PR #12567: [build] Split stdlib to it's own package.coqbot-app[bot]
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-03-02Merge PR #13889: Dead code elimination: not reducible error message is never ...coqbot-app[bot]
2021-03-02Merge PR #13891: Simplify installation instructions in README.coqbot-app[bot]
2021-03-02Simplify wording.Théo Zimmermann
2021-03-02Simplify installation instructions in README.Théo Zimmermann
2021-03-02Dead code elimination: not reducible error message is never raised.Théo Zimmermann
2021-02-28Merge PR #13853: Delay the dynamic linking of native-code libraries until nat...Pierre-Marie Pédrot
2021-02-28Merge PR #13886: Correct broken link.coqbot-app[bot]
2021-02-28Fix link of default_bindings.slb Prime
2021-02-27Merge PR #13876: [coqc] Don't allow to pass more than one file to coqccoqbot-app[bot]
2021-02-27Add overlayPierre Roux
2021-02-27Add changelogPierre Roux
2021-02-27Remove decimal-only number notationsPierre Roux
2021-02-27Merge PR #13559: Signed primitive integerscoqbot-app[bot]
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
2021-02-26Merge PR #13884: CI Windows: adjust branch name to Coq Platform branch renamingcoqbot-app[bot]
2021-02-26Merge PR #13883: Expose Top_printers.econstr_displaycoqbot-app[bot]
2021-02-26CI Windows: adjust branch name to Coq Platform branch renamingMichael Soegtrop
2021-02-26Expose Top_printers.econstr_displayGaëtan Gilbert
2021-02-26Signed primitive integersAna
2021-02-26Merge PR #13869: Use make_case_or_project in auto_ind_declPierre-Marie Pédrot
2021-02-26Merge PR #13676: Protect caml_process_pending_actions_exn with caml_something...Pierre-Marie Pédrot
2021-02-26Merge PR #13868: Make genOpcodeFiles.ml handle opcode arity.Pierre-Marie Pédrot
2021-02-26Delay the dynamic linking of native-code libraries until native_compute is ca...Guillaume Melquiond
2021-02-25Merge PR #13393: [proof using] Remove duplicate code, refactor.coqbot-app[bot]
2021-02-25[proof using] Remove duplicate code, refactor.Emilio Jesus Gallego Arias
2021-02-25Merge PR #13202: Infrastructure for fine-grained debug flagscoqbot-app[bot]
2021-02-25Merge PR #13863: Get rid of the compilation date from the binaries to make th...coqbot-app[bot]
2021-02-25Merge PR #13080: Ascii: add leb and ltbcoqbot-app[bot]
2021-02-25Merge PR #13738: Make sure Ltac2 get cleaned too.coqbot-app[bot]
2021-02-24Overlay for Set DebugGaëtan Gilbert
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-23Print anomaly labels regardless of -debug, and never print user_err labelsGaëtan Gilbert
2021-02-23Merge PR #13880: Fix the release process checklist with respect to the refman...coqbot-app[bot]