aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-20Granting #9816: apply in takes several hypotheses.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-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-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-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-17Merge PR #13390: Intern application arguments in left-to-right ordercoqbot-app[bot]
2020-11-17Merge PR #13397: Adding heterogeneous map on named contexts.Pierre-Marie Pédrot
2020-11-17Merge PR #13404: Persistent_cache.t is always OpenPierre-Marie Pédrot
2020-11-17Adding change log for #12984.Hugo Herbelin
2020-11-17Documenting priority given to most recently declared/imported notations.Hugo Herbelin
2020-11-17A reimport of notations now put the corresponding notations again in front.Hugo Herbelin
2020-11-17Add changelog for #12986.Hugo Herbelin
2020-11-17Documenting the preference given to more precise notations at printing time.Hugo Herbelin
2020-11-17For printing, ordering notations by precision of the pattern.Hugo Herbelin
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
2020-11-17Merge PR #13402: [ci] Use lite target for Perennialcoqbot-app[bot]
2020-11-17[ci] Use lite target for PerennialTej Chajed
2020-11-17Persistent_cache.t is always OpenGaëtan Gilbert
2020-11-16Adding Array.iter3.Hugo Herbelin
2020-11-16Fixing alpha-equality of notation interpretations with recursive patterns.Hugo Herbelin
2020-11-16[doc] add a link to v8.13Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:06:09 +0000