Sebastian Graf 36eaa68744 fix: make all VCs emitted by mvcgen synthetic opaque (#12048) ... This PR fixes a bug where `mvcgen` loses VCs, resulting in unassigned metavariables. It is fixed by making all emitted VCs synthetic opaque. The bug was reported by [Alexander Bentkamp on the community Zulip](https://leanprover.zulipchat.com/#narrow/channel/236449-Program-verification/topic/mvcgen.20bug.3F.20.22declaration.20has.20metavariables.22).		2026-01-19 16:51:10 +00:00
..
bin
cmake
include/lean	feat: add a symbol gadget for non linear Array copies (#11916)	2026-01-07 13:08:45 +00:00
Init	chore: minor fixups in String.ofList (#12043)	2026-01-19 09:25:47 +00:00
initialize	feat: zero cost BaseIO (#10625)	2025-10-22 10:55:12 +02:00
kernel	perf: Options.hasTrace (#12001)	2026-01-16 09:03:40 +00:00
lake	feat: add lake shake command (#11921)	2026-01-19 11:11:13 +00:00
Lean	fix: make all VCs emitted by mvcgen synthetic opaque (#12048)	2026-01-19 16:51:10 +00:00
LeanChecker	feat: re-integrate lean4checker as leanchecker (#11887)	2026-01-08 09:41:33 +00:00
library	perf: avoid allocation on lean_trace use in interpreter (#12036)	2026-01-18 19:33:48 +00:00
runtime	chore: fix Windows build (#11988)	2026-01-13 13:06:38 +00:00
shell	chore: tests: use filenames as test names (#11302)	2025-11-21 12:40:58 +00:00
Std	chore: remove unused example in clz bitblasting circuit (#11989)	2026-01-13 11:45:24 +00:00
util	perf: avoid allocation on lean_trace use in interpreter (#12036)	2026-01-18 19:33:48 +00:00
cadical.mk
CMakeLists.txt	perf: garbage-collect dead sections (#1700)	2026-01-15 16:39:46 +00:00
config.h.in
githash.h.in
Init.lean	feat: add Sym.Simp.evalGround simproc (#12031)	2026-01-17 05:13:12 +00:00
lakefile.toml.in	feat: re-integrate lean4checker as leanchecker (#11887)	2026-01-08 09:41:33 +00:00
lean-toolchain
Lean.lean	refactor: move error explanation text to the manual (#11688)	2025-12-26 17:14:58 +00:00
lean.mk.in
Leanc.lean
LeanChecker.lean	feat: re-integrate lean4checker as leanchecker (#11887)	2026-01-08 09:41:33 +00:00
out
Std.lean	chore: more module system fixes and refinements for finishing batteries port (#10819)	2025-10-21 08:19:50 +00:00
stdlib.make.in	feat: re-integrate lean4checker as leanchecker (#11887)	2026-01-08 09:41:33 +00:00
stdlib_flags.h	chore: remove comment from wrong stdlib_flags.h (#11646)	2025-12-12 22:59:38 +00:00
version.h.in