From 0a6cbb08548d71e6557116a7d187f067a6ec374d Mon Sep 17 00:00:00 2001 From: Ralf Jung <post@ralfj.de> Date: Mon, 25 Jan 2016 10:59:52 +0100 Subject: [PATCH] README: add note about Ssreflect and bullets --- README | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README b/README index b10db0a41..5e2238711 100644 --- a/README +++ b/README @@ -6,6 +6,11 @@ This version is known to compile with: - Coq 8.5 - Ssreflect 1.6 - Autosubst 1.4 + +For development, better make sure you have a version of Ssreflect that includes commit be724937 +(no such version has been released so far, you'll have to fetch the development branch yourself). +Iris compiles fine even without this patch, but proof bullets will only be in 'strict' (enforcing) +mode with the fixed version of Ssreflect. BUILDING INSTRUCTIONS --------------------- -- GitLab