Coq

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

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

Branch merges

Branch information

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

Recent commits

eaeb14e... by Jason Gross

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

599c0af... 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>

0106ca8... by Hugo Herbelin <email address hidden>

Updating CHANGES about critical VM and universes bug.

05edbd0... by =?utf-8?b?TWF4aW1lIETDqW7DqHM=?= <email address hidden>

Add test case for #6677.

Cherry-pick of 1ee8511 from v8.6 and of 07e861c1 from master.

a2cc54c... by =?utf-8?b?TWF4aW1lIETDqW7DqHM=?= <email address hidden>

Fix #6677: Critical bug with VM and universes

This bug was present since the first patch adding universe polymorphism
handling in the VM (Coq 8.5). Note that unsoundness can probably be
observed even without universe polymorphism.

This is an adaptation of a cherry-pick of d4d550d0 from v8.5 which
itself is an adaptation of c9f3a6c in master (PR #6713).

64db508... by =?utf-8?b?TWF4aW1lIETDqW7DqHM=?= <email address hidden>

Merge PR #6348: Compatibility of 8.6 with OCaml 4.06.0.

9add036... by Hugo Herbelin <email address hidden>

Configure: Support for unsafe-string compatibility with OCaml 4.06.0.

d84189d... by Hugo Herbelin <email address hidden>

Documenting need for num library when compiling with 4.06.

6f4bbaa... by Paul Steckler

check for Num lib if OCaml >= 4.06, #6162

2a4c764... by =?utf-8?q?Th=C3=A9o_Zimmermann?= <email address hidden>

These developments have moved on to 8.7.