diff --git a/src/extraction/FStar.Extraction.Kremlin.fs b/src/extraction/FStar.Extraction.Kremlin.fs
index d6d215937e4..4d293d61239 100644
--- a/src/extraction/FStar.Extraction.Kremlin.fs
+++ b/src/extraction/FStar.Extraction.Kremlin.fs
@@ -55,6 +55,7 @@ and decl =
   | DTypeVariant of lident * list<flag> * int * branches_t
   | DTypeAbstractStruct of lident
   | DExternal of option<cc> * list<flag> * lident * typ * list<ident>
+  | DUntaggedUnion of lident * list<flag> * int * list<(ident * typ)>
 
 and cc =
   | StdCall