aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-20Merge PR #13399: Miscellaneous ring improvements in code + error messagesPierre-Marie Pédrot
2020-11-20add perennial to benchmark suiteRalf Jung
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
2020-11-20Merge PR #13305: Only lower inductives to Prop if the type is syntactically a...Pierre-Marie Pédrot
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Adding change log.Hugo Herbelin
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-20Merge PR #13360: Fix incorrect name refreshing when interning a generalized b...coqbot-app[bot]
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
2020-11-20[doc] [ssr] fix documentation of reflectEnrico Tassi
2020-11-20Update doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars...Hugo Herbelin
2020-11-20Merge PR #13386: Fixes #9971: a useless situation where the type of a primiti...coqbot-app[bot]
2020-11-20Merge PR #13371: Extend hack to use postponed constraints in retyping to temp...coqbot-app[bot]
2020-11-20[stm] [declare] Remove pinfo internals hack.Emilio Jesus Gallego Arias
2020-11-20[stm] [declare] Try to propagate safe bits of proof informationEmilio Jesus Gallego Arias
2020-11-19Adding changelog for #13237.Hugo Herbelin
2020-11-19Merge PR #13423: [changelog] Indicate a replacement for deprecated syntax of ...coqbot-app[bot]
2020-11-19[changelog] Indicate a replacement for deprecated syntax of debug / info_eauto.Théo Zimmermann
2020-11-19Add overlays for elpi and unicoq.Hugo Herbelin
2020-11-19Add changelog for #13386.Hugo Herbelin
2020-11-19Use a proper canonical structure entry for projections.Hugo Herbelin
2020-11-19Fixes #9971: expand_projections failing on primitive projections of unknown t...Hugo Herbelin
2020-11-19Merge PR #13421: Fix typo in rst link syntax.coqbot-app[bot]
2020-11-19Fix typo in rst link syntax.Théo Zimmermann
2020-11-19Merge PR #12959: Improve the bytecode interpreterPierre-Marie Pédrot
2020-11-19Modular printing algorithm for bench/render_results.Pierre-Marie Pédrot
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ...coqbot-app[bot]
2020-11-18Merge PR #13312: [attributes] Allow boolean, single-value attributes.coqbot-app[bot]
2020-11-18Merge PR #13389: [ci/gitlab/windows] Do not load user overlays.Michael Soegtrop
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-18Merge PR #13410: [configure] check that zarith dev files are availablecoqbot-app[bot]
2020-11-18[configure] check that zarith dev files are availableEnrico Tassi
2020-11-18[attributes] Add output test suite for errors, improve error printing.Emilio Jesus Gallego Arias
2020-11-18[attributes] Update error message referring to deprecated syntax.Emilio Jesus Gallego Arias
2020-11-18Review commit: improving the doc of boolean attributes.Théo Zimmermann
2020-11-18Run doc_grammar for #13312.Théo Zimmermann
2020-11-18[attributes] Add overlays for #13312Emilio Jesus Gallego Arias
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
2020-11-18Merge PR #13400: [doc] add a link to v8.13coqbot-app[bot]
2020-11-18Add more explicit tests for next_up and next_down.Pierre Roux
2020-11-18[attributes] Allow boolean, single-value attributes.Emilio Jesus Gallego Arias
2020-11-18Merge PR #13220: Give a typical example of Makefile wrapper for coq_makefile ...coqbot-app[bot]
2020-11-18Merge PR #12765: In recursive notations, accept partial application over the ...coqbot-app[bot]
2020-11-18Merge PR #13341: Finish fixing setoid rewrite under anonymous lambdas (hopefu...Pierre-Marie Pédrot
2020-11-18Merge PR #13251: Make sure that setoid_rewrite passes state to subgoalsPierre-Marie Pédrot
2020-11-18Update doc/sphinx/practical-tools/utilities.rstHugo Herbelin
2020-11-18Ref. man.: showing the x ⪯ y ⪯ .. ⪯ z ⪯ t example of recursive notation.Hugo Herbelin
2020-11-18Adding change log for #12765.Hugo Herbelin
2020-11-18In recursive notations, accept partial application over the recursive pattern.Hugo Herbelin
2020-11-18[micromega] Updated test-suiteBESSON Frederic
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 19:51:46 +0000