Coq

~jgross-h/coq/+git/coq:v8.13

  1. Git
  2. lp:~jgross-h/coq/+git/coq
  3. v8.13
Last commit made on 2022-07-01
Get this branch:
git clone -b v8.13 https://git.launchpad.net/~jgross-h/coq/+git/coq

Branch merges

Branch information

Name:
v8.13
Repository:
lp:~jgross-h/coq/+git/coq

Recent commits

02e434a... by Jason Gross

Merge PR #16232: [v8.13] Backport #15271: Delay removing native_compute .ml files until exit

ee08da0... by Jason Gross

Put "v8.13" in CACHEKEY

Co-authored-by: Gaëtan Gilbert <email address hidden>

70a70bc... by =?utf-8?q?Ga=C3=ABtan_Gilbert?= <email address hidden>

Delay removing native_compute .ml files until exit

Fix #15263 (assuming it was correctly diagnosed)

Co-authored-by: Jason Gross <email address hidden>

34da65a... by Enrico Tassi

update version to 8.13.2

995a0d4... by Enrico Tassi

Backport PR #14044: [RM] changelog for 8.13.2

297294e... by Enrico Tassi

changelog for 8.13.2

(cherry picked from commit 39e3201c01b1a8baec279ccdc7a8acb3a341c3dd)

06f6cae... by Enrico Tassi

Backport PR #14012: Fix Ltac2 `Array.init` exponential overhead

6b851b4... by Jason Gross

Fix Ltac2 `Array.init` exponential overhead

Previously, `Array.init` was computing the first element of the array
twice, resulting in exponential overhead in the number of recursive
nestings of `Array.init`. Notably, since `Array.map` is implemented in
terms of `Array.init`, this exponential blowup shows up in any term
traversal based on `Array.map` over the arguments of application nodes.

Fixes #14011

(cherry picked from commit 7e5dc9f830bc2cdbc3b8cc8b830adafc61660055)

1ec33b0... by Enrico Tassi

Backport PR #14005: Support OCaml primitives with an actual arity larger than 4.

f2577b3... by Guillaume Melquiond <email address hidden>

Document as critical.

(cherry picked from commit 7ff8b12c14867e43d54c3d4c8976a6179250893d)