Coq

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

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

Branch merges

Branch information

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

Recent commits

25fcbe6... by Jason Gross

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

9b4e18a... 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>

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

Merge PR #13607: [v8.12] 8.12.2 release

Ack-by: jfehrle

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

Bump version number to 8.12.2.

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

Changelog for 8.12.2.

(cherry picked from commit 1e37c5234f3237eeb7fef85d461e6b8108cd0edf)

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

Backport PR #13468: Fixes #13456: regression in tactic exists which started to check resolution of evars more incrementally

279e320... by Hugo Herbelin <email address hidden>

Fixes #13456: regression where tactic exists started to check evars incrementally.

The regression was due to #12365. We fix it by postponing the evars
check after the calls to the underlying constructor tactic, while
retaining using information from the first instantiations to resolve
the latter instantiations.

(cherry picked from commit e353fe431351bb1f41bc6a8c813bea980e8d247c)

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

Backport PR #13473: Testing {in _, _} and {pred _} from ssrbool

831c47d... by Cyril Cohen <email address hidden>

Testing {in _, _} and {pred _} from ssrbool

(cherry picked from commit 36664ba0ac77968037687634af0cd5a808335cfc)

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

Backport PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a coercion not being used