aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-17Fixes #13235: remove fragile tolerance for degenerate in-hyps clause.Hugo Herbelin
2020-11-16Improve some error messages.Vincent Semeria
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
2020-11-16Other renamings evd -> sigma in newring.ml.Hugo Herbelin
2020-11-16Pass sigma functionally in newring.ml.Hugo Herbelin
2020-11-16Merge PR #12873: Unification: A type-checking fix in imitation + an error loc...coqbot-app[bot]
2020-11-16Adding heterogeneous map on named contexts.Hugo Herbelin
2020-11-16Improve bad variance error message: mention expected and actual variancesGaëtan Gilbert
2020-11-16Merge PR #13040: [gc] Set GC policy as best-fit in OCaml >= 4.10.0coqbot-app[bot]
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
2020-11-16Using labels to document match_notation_constr.Hugo Herbelin
2020-11-16Add change log for #12965.Hugo Herbelin
2020-11-16Fix #9569 (notations collect the spine binding variables at printing time).Hugo Herbelin
2020-11-16Merge PR #13212: Suggesting to use injection when an injection pattern is giv...coqbot-app[bot]
2020-11-16Merge PR #13380: Fixing the "IllTypedInstance" anomaly part of #5512coqbot-app[bot]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 06:56:50 +0000