From 53fa71ca194c391abb53b0999fbe4643a5c57428 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Dec 2015 13:34:59 +0100
Subject: [PATCH] Make solution of cofe solver opaque.

---
 iris/cofe_solver.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/iris/cofe_solver.v b/iris/cofe_solver.v
index 81b86c3cf..0610e1f3d 100644
--- a/iris/cofe_solver.v
+++ b/iris/cofe_solver.v
@@ -228,3 +228,5 @@ Proof.
   apply dist_S, map_contractive; split; intros Y i; apply embed_tower; lia.
 Qed.
 End solver.
+
+Global Opaque cofe_solver.T cofe_solver.fold cofe_solver.unfold.
-- 
GitLab