comment out all viperproject#1221 specs for now

juliand665 · Feb 15, 2023 · 0b2a7d8 · 0b2a7d8
1 parent 077c0e0
commit 0b2a7d8
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/prusti-contracts/prusti-contracts/src/core_spec/ops/index.rs b/prusti-contracts/prusti-contracts/src/core_spec/ops/index.rs
@@ -4,8 +4,10 @@ use crate::*;
 use core::ops::Index;
 
 // FUTURE(#1221): This spec is currently not usable due to issue #1221.
+/*
 #[extern_spec]
 trait Index<Idx> {
     #[pure]
     fn index(&self, idx: Idx) -> &Self::Output;
 }
+*/
diff --git a/prusti-contracts/prusti-contracts/src/core_spec/slice.rs b/prusti-contracts/prusti-contracts/src/core_spec/slice.rs
@@ -42,6 +42,7 @@ impl<T> [T] {
 }
 
 // FUTURE(#1221): This spec is currently not usable due to issue #1221.
+/*
 #[extern_spec]
 impl<T, I> Index<I> for [T]
 where
@@ -50,3 +51,4 @@ where
     #[pure]
     fn index(&self, index: I) -> &I::Output;
 }
+*/