aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-09-30Merge PR #13032: More precise information when unification fails because of ↵Pierre-Marie Pédrot
incompatible candidates Reviewed-by: ppedrot
2020-09-29Merge PR #13111: Small document fixes.coqbot-app[bot]
Reviewed-by: jfehrle
2020-09-30Wf.v defines Fix_eq, not fix_eq.Tanaka Akira
A commit at 2003-03-13 changed the lemma name. https://github.com/coq/coq/commit/cb1ae314411d78952062e5092804b85d981ad6e1
2020-09-30Type{i} should be Type(i).Tanaka Akira
2020-09-29Merge PR #13101: Reduce nitpick_ignore list a little.Clément Pit-Claudel
2020-09-29Merge PR #13097: Modify how quotations handle whole sentences.coqbot-app[bot]
Reviewed-by: gares
2020-09-29Merge PR #13039: Lint stdlib with -mangle-names #3coqbot-app[bot]
Reviewed-by: anton-trunov
2020-09-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a ↵coqbot-app[bot]
lonely notation at printing time. Reviewed-by: ejgallego Ack-by: maximedenes
2020-09-28Merge PR #13105: [nix] CI script wrapper now requires Pythoncoqbot-app[bot]
Reviewed-by: vbgl
2020-09-28Merge PR #13053: [lib] make canonical_path_name always absolute (fix #13031)Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-28More precise information when unification fails because of incompatible ↵Hugo Herbelin
candidates. We also show the incompatible contender. Ideally, we should also remember the source of the other contender.
2020-09-28CI script wrapper now requires PythonMaxime Dénès
2020-09-27Avoid lookup up too many characters.Guillaume Melquiond
This would cause issues in noninteractive mode. For example, when using Drop, the first character of the OCaml code would be read by Coq's REPL instead of OCaml's REPL. The peek_string function is quite inefficient, since the Stream module does not provide any good function to lookup arbitrary characters (or to push back characters).
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
2020-09-27Recognize only ":{{" as a sentence-gobbling quotation.Guillaume Melquiond
2020-09-27Make "xxx:{{" always start a quotation, whether registered or not.Guillaume Melquiond
This commit also prevents quotations using "(" and "[" from gobbling sentences. As a consequence, dynamically-registered quotations can no longer modify where Coq sentences stop.
2020-09-25Merge PR #12999: More improvements in locating tactic errorscoqbot-app[bot]
Reviewed-by: ppedrot Reviewed-by: ejgallego
2020-09-24Merge PR #12894: Modify bytecode representation of closures to please OCamls ↵coqbot-app[bot]
GC (fix #12636). Reviewed-by: maximedenes Ack-by: bgregoir Ack-by: proux01
2020-09-24Merge PR #13077: Fix issue #13065 - Windows CI brokencoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-23Fix issue #13065 - Windows CI brokenMichael Soegtrop
2020-09-23Merge PR #12977: Statically ensure that only polymophic hint terms come with ↵coqbot-app[bot]
a context. Reviewed-by: mattam82
2020-09-23Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)coqbot-app[bot]
Reviewed-by: ejgallego
2020-09-23Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of ↵Pierre-Marie Pédrot
quotations at printing time Reviewed-by: ppedrot
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-22Merge PR #13061: fix build:quick and build:base+async artifactscoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-22Merge PR #13067: Setting default value for Display Parentheses off in CoqIDEcoqbot-app[bot]
Reviewed-by: ejgallego
2020-09-22Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested ↵coqbot-app[bot]
applications in notations Reviewed-by: ejgallego Ack-by: maximedenes
2020-09-22Adding change log for #12794 and #13067.Hugo Herbelin
2020-09-22Setting default value for Display Parentheses off in CoqIDE.Hugo Herbelin
2020-09-22Add overlay for Equations.Hugo Herbelin
2020-09-22Adding change log for #13028.Hugo Herbelin
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-22Use the closure tag for accumulators.Guillaume Melquiond
The first field of accumulators points out of the OCaml heap, so using closures instead of tag-0 objects is better for the GC. Accumulators are distinguished from closures because their code pointer necessarily is the "accumulate" address, which points to an ACCUMULATE instruction.
2020-09-22Use the same memory layout as closures for accumulators.Guillaume Melquiond
That way, accumulators again can be used directly as execution environments by the bytecode interpreter. This fixes the issue of the first argument of accumulators being dropped when strongly normalizing.
2020-09-22Modify bytecode representation of closures to please OCaml's GC (fix #12636).Guillaume Melquiond
The second field of a closure can no longer be the value of the first free variable (or another closure of a mutually recursive block) but must be an offset to the first free variable. This commit makes the bytecode compiler and interpreter agnostic to the actual representation of closures. To do so, the execution environment (variable coq_env) no longer points to the currently executed closure but to the last one. This has the following consequences: - OFFSETCLOSURE(n) now always loads the n-th closure of a recursive block (counted from last to first); - ENVACC(n) now always loads the value of the n-th free variable. These two changes make the bytecode compiler simpler, since it no longer has to track the relative position of closures and free variables. The last change makes the interpreter a bit slower, since it has to adjust coq_env when executing GRABREC. Hopefully, cache locality will make the overhead negligible.
2020-09-22Merge PR #13046: Small optimization of acyclic graph merge operationcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-22Merge PR #13050: [ci/gitlab/cachix] Avoid running in trouble when calling ↵coqbot-app[bot]
git fetch --unshallow Reviewed-by: SkySkimmer
2020-09-22Merge PR #13049: [configure] Fix version checks for lablgtk and zarithcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: vbgl Ack-by: Zimmi48 Ack-by: JasonGross
2020-09-22Merge PR #13063: Make print-pretty-timed robust against non-output-sync logscoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-21Merge PR #13057: Adding debugging printers for Intmapcoqbot-app[bot]
Reviewed-by: ppedrot
2020-09-21Make print-pretty-timed robust against non-output-sync logsJason Gross
Also pass `--output-sync` on the CI, as suggested in https://github.com/coq/coq/pull/12653#issuecomment-696226093, to protect against this failure mode. Fixes #13062
2020-09-21Bump nixpkgs to get zarith 1.10.Théo Zimmermann
2020-09-21Merge PR #12723: dune: pass -bin-annot to configurecoqbot-app[bot]
Reviewed-by: ejgallego
2020-09-21fix build:quick and build:base+async artifactsGaëtan Gilbert
We put dmesg.txt in the artifact path for all build-template users, but only these 2 jobs produce it to avoid uploading unused data (see discussion in #13043).
2020-09-19Merge PR #13052: Clean up Dnet implementationHugo Herbelin
Reviewed-by: herbelin
2020-09-18Merge PR #13055: Fix Removed in Sphinx 4 deprecations.coqbot-app[bot]
Reviewed-by: jfehrle
2020-09-18Merge PR #12963: Formally deprecate the double induction tactic.Hugo Herbelin
Reviewed-by: VincentSe Ack-by: herbelin Ack-by: olaure01
2020-09-18Adding debugging printers for Intmap.Hugo Herbelin
2020-09-18Merge PR #13051: Improve `simple apply` examplecoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-18Merge PR #13043: [ci] call dmesg after quick/async jobs to detect OOMcoqbot-app[bot]
Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:59:23 +0000