aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-03-10Regenerate the Ltac2 syntax for documentation.Pierre-Marie Pédrot
2021-03-10Adding documentation of the changes.Pierre-Marie Pédrot
2021-03-10Adding a parsing test.Pierre-Marie Pédrot
2021-03-10Allow the presence of type casts for return values in Ltac2.Pierre-Marie Pédrot
2021-03-10Merge PR #13912: Refactor coercionopscoqbot-app[bot]
2021-03-10Merge PR #13919: Fix a hyperlink in CONTRIBUTING.mdcoqbot-app[bot]
2021-03-10Fix a hyperlink in CONTRIBUTING.mdKazuhiko Sakaguchi
2021-03-09Add changelogKazuhiko Sakaguchi
2021-03-09Add overlayKazuhiko Sakaguchi
2021-03-09Add the source and target classes to the coercion tableKazuhiko Sakaguchi
2021-03-09Replace cl_index with cl_typ in coercionops.mlKazuhiko Sakaguchi
2021-03-08Merge PR #13707: Convert 2nd part of rewriting chapter to prodncoqbot-app[bot]
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-03-07Merge PR #13910: Attempt to fix the bench after coq-core splitPierre-Marie Pédrot
2021-03-07Attempt to fix the bench after coq-core splitGaëtan Gilbert
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-05Update nixpkgs.Théo Zimmermann
2021-03-05Fix the .mailmap.Théo Zimmermann
2021-03-05Document the relation of the list-contributors.sh script to .mailmap.Théo Zimmermann
2021-03-05Fix list-constributors.sh script.Théo Zimmermann
2021-03-05Merge PR #13900: doc: don't count a contributor twice in the changelogcoqbot-app[bot]
2021-03-04Correctly sort the glossaryJim Fehrle
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-04[test-suite] test for primitive tokens in patternsEnrico Tassi
2021-03-04[doc] changelog entryEnrico Tassi
2021-03-04[doc] Set/Unset Printing Raw LiteralsEnrico Tassi
2021-03-04[notation] option to fine tune printing of literalsEnrico Tassi
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]
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 20:31:51 +0000