From 0804b50571f447616644018290ee8151543f2311 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 25 Aug 2026 23:12:56 +0000 Subject: [PATCH] docs: make consumer guidance integration-neutral --- README.md | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 9994f3b..70103ab 100644 --- a/README.md +++ b/README.md @@ -23,9 +23,7 @@ The benchmark context is still required in schema version 1 to resolve trusted i modules and declaration spans from `.ilean` data. A future wire version can replace that context with an explicit dependency bundle without changing schema version 1. -The consumer owns hole resolution. This matches the interface needed by the -Formal Conjectures importer: it can resolve declarations under LeanEval's -pinned target environment, then pass the resulting ranges and dependency data -to this renderer. Formal Conjectures fixtures are intentionally not copied or -modified in this foundation package; they should be added by their importer -owners when that consumer switches to the contract. +The consumer owns hole resolution. A consumer resolves declarations under its +pinned target environment, then passes the resulting ranges and dependency +data to this renderer. Consumer-specific fixtures and source trees do not +belong in this foundation package.