What would need to work to fix this

FStarLang · Feb 20, 2025 · 4302112 · 4302112
1 parent 62907a1
commit 4302112
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git 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
@@ -1,5 +1,6 @@
 module AbstractStructAbstract
 
+[@CAbstractStruct]
 val t (a:Type0) : Type0
 
 val make (#a:Type0) (x:a) : t a