Coq

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

  1. Git
  2. lp:~jgross-h/coq/+git/coq
  3. v8.5
Last commit made on 2023-04-03
Get this branch:
git clone -b v8.5 https://git.launchpad.net/~jgross-h/coq/+git/coq

Branch merges

Branch information

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

Recent commits

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

v8.5: Fix CAMLP4DEPS invocation

The old one worked on bash but not eg debian dash (/bin/sh)

017b3b3... by Jason Gross

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

d834811... 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>

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

Updating CHANGES about critical VM and universes bug.

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

Add test case for #6677.

Cherry-pick of 07e861c1 from master.

d4d550d... 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 the adaptation of a cherry-pick of c9f3a6cbe5c41 in master (PR #6713).

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

Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in batch mode.

5dd2e57... by Pierre Letouzey

configure: avoid deprecated warnings

4623cde... by Hugo Herbelin <email address hidden>

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

79393ba... by Hugo Herbelin <email address hidden>

Documenting need for num library when compiling with 4.06.