aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-19Modular printing algorithm for bench/render_results.Pierre-Marie Pédrot
The old code was a mess of handwritten ad-hoc code to print the result table in a fancy way. Instead of hardcoding everything this patch introduces a generic function to print a table of data. This will allow extension of the profiling information displayed to the user in an easy way.
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ↵coqbot-app[bot]
then by last imported Reviewed-by: Zimmi48 Ack-by: RalfJung Ack-by: gares
2020-11-18Merge PR #13312: [attributes] Allow boolean, single-value attributes.coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: SkySkimmer Ack-by: gares
2020-11-18Merge PR #13389: [ci/gitlab/windows] Do not load user overlays.Michael Soegtrop
Reviewed-by: MSoegtropIMC
2020-11-18Merge PR #13410: [configure] check that zarith dev files are availablecoqbot-app[bot]
Reviewed-by: ejgallego Ack-by: silene
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
We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog.
2020-11-18Merge PR #13400: [doc] add a link to v8.13coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-18[attributes] Allow boolean, single-value attributes.Emilio Jesus Gallego Arias
Following discussion in https://github.com/coq/coq/pull/12586 , we extend the syntax `val=string` to support also arbitrary values. In particular we support boolean ones, or arbitrary key-pair lists. This complements the current form `val="string"`, and makes more sense in general. Current syntax for the boolean version is `attr=yes` or `attr=no`, but we could be more liberal if desired. The general new guideline is that `foo(vals)` is reserved for the case where `vals` is a list, whereas `foo=val` is for attributes that allow a unique assignment. This commit only introduces the support, next commits will migrate some attributes to this new syntax and deprecate the old versions.
2020-11-18Merge PR #13220: Give a typical example of Makefile wrapper for coq_makefile ↵coqbot-app[bot]
(addresses #12903) Reviewed-by: gares Ack-by: Zimmi48 Ack-by: SkySkimmer
2020-11-18Merge PR #12765: In recursive notations, accept partial application over the ↵coqbot-app[bot]
recursive pattern Reviewed-by: gares Ack-by: maximedenes Ack-by: jfehrle
2020-11-18Merge PR #13341: Finish fixing setoid rewrite under anonymous lambdas ↵Pierre-Marie Pédrot
(hopefully) Reviewed-by: ppedrot
2020-11-18Merge PR #13251: Make sure that setoid_rewrite passes state to subgoalsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-18Update doc/sphinx/practical-tools/utilities.rstHugo Herbelin
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
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
This allows e.g. to support a notation of the form "x <== y <== z <= t" standing for "x <= y /\ y <= z /\ z <= t".
2020-11-17Merge PR #13390: Intern application arguments in left-to-right ordercoqbot-app[bot]
Reviewed-by: herbelin
2020-11-17Merge PR #13397: Adding heterogeneous map on named contexts.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-17Merge PR #13404: Persistent_cache.t is always OpenPierre-Marie Pédrot
Reviewed-by: fajb
2020-11-17Adding change log for #12984.Hugo Herbelin
Co-authored-by: Ralf Jung <post@ralfj.de>
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
This relies on finer-than partial order check with. In particular: - number and order of notation metavariables does not matter - take care of recursive patterns inclusion
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: ppedrot
2020-11-17Merge PR #13402: [ci] Use lite target for Perennialcoqbot-app[bot]
Reviewed-by: SkySkimmer
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
The name bound in binders were not checked up to alpha-equivalence, nor were the names binding the recursive patterns.
2020-11-16[doc] add a link to v8.13Enrico Tassi
2020-11-16Merge PR #12873: Unification: A type-checking fix in imitation + an error ↵coqbot-app[bot]
locating fix Reviewed-by: gares
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]
Reviewed-by: gares Reviewed-by: ppedrot
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Merge PR #13212: Suggesting to use injection when an injection pattern is ↵coqbot-app[bot]
given to destruct (wish #13205) Reviewed-by: gares Ack-by: Blaisorblade Ack-by: RalfJung
2020-11-16Merge PR #13380: Fixing the "IllTypedInstance" anomaly part of #5512coqbot-app[bot]
Reviewed-by: gares
2020-11-16Suggesting to use injection when an injection pattern is given to destruct.Hugo Herbelin
This hopefully clarifies the confusing role of destruct (see #13205).
2020-11-16[gc] Set GC policy as best-fit in OCaml >= 4.10.0Emilio Jesus Gallego Arias
Closes #11277 ; the `space_overhead` parameter has been selected for maximum speedup, in some cases it could also increase memory consumption. Please use `OCAMLRUNPARAM` to tune it and report back your experiments.
2020-11-16Merge PR #12690: Mini-fix of Locate for recursive notations using named ↵coqbot-app[bot]
variables. Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: SkySkimmer
2020-11-16Merge PR #13337: Avoid exposing an internal name when "intros _ H" fails ↵coqbot-app[bot]
because of _ being dependent in H Reviewed-by: gares
2020-11-16Add changelog for #13337.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 01:05:50 +0000