Commented lemma cap_invalidate_preserves_bounds to avoid extraction i…

…ssues
rems-project · Mar 27, 2024 · c19d0d1 · c19d0d1
1 parent bb46061
commit c19d0d1
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v
@@ -1098,9 +1098,9 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
     bv_simplify. rewrite bv_extract_unsigned. rewrite bv_extract_unsigned. bv_simplify.  bitblast.       
     Qed.  
 
-  Lemma cap_invalidate_preserves_bounds (c:t) : cap_get_bounds c = cap_get_bounds (cap_invalidate c).
+  (* Lemma cap_invalidate_preserves_bounds (c:t) : cap_get_bounds c = cap_get_bounds (cap_invalidate c).
   Proof.
-      Admitted.
+      Admitted. *)
 
 End Capability.