From 43021128f00ff2b26435b656850a8741a630d190 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Thu, 20 Feb 2025 14:57:19 -0500
Subject: [PATCH] What would need to work to fix this

---
 test/AbstractStruct2.fst         | 2 +-
 test/AbstractStructAbstract.fsti | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/test/AbstractStruct2.fst b/test/AbstractStruct2.fst
index 70cd179cf..921a69cbe 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 787cafe8d..72424aec0 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