diff --git a/test/AbstractStruct2.fst b/test/AbstractStruct2.fst
index 70cd179c..921a69cb 100644
--- a/test/AbstractStruct2.fst
+++ b/test/AbstractStruct2.fst
@@ -4,7 +4,7 @@ module B = LowStar.Buffer
 
 open FStar.HyperStack.ST
 
-[@@CAbstractStruct]
+[@CAbstractStruct]
 noeq
 type handle = {
   something: bool;
diff --git a/test/AbstractStructAbstract.fsti b/test/AbstractStructAbstract.fsti
index 787cafe8..72424aec 100644
--- a/test/AbstractStructAbstract.fsti
+++ b/test/AbstractStructAbstract.fsti
@@ -1,5 +1,6 @@
 module AbstractStructAbstract
 
+[@CAbstractStruct]
 val t (a:Type0) : Type0
 
 val make (#a:Type0) (x:a) : t a