From ef59256fb354edb9d6ffee81bb3f9e82648a6d5a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 8 Feb 2022 18:14:13 +0100
Subject: Fix some issues

---
 src/ExtractToFStar.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'src/ExtractToFStar.ml')

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index db09b316..aecd6c68 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -95,7 +95,7 @@ let fstar_keywords =
   List.concat [ named_unops; named_binops; misc ]
 
 let fstar_assumed_adts : (assumed_ty * string) list =
-  [ (Result, "result"); (Option, "option") ]
+  [ (Result, "result"); (Option, "option"); (Vec, "vec") ]
 
 let fstar_assumed_structs : (assumed_ty * string) list = []
 
@@ -397,7 +397,13 @@ let extract_type_def_register_names (ctx : extraction_ctx) (def : type_def) :
   let ctx =
     match def.kind with
     | Struct fields ->
-        fst (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx)
+        (* Add the fields *)
+        let ctx =
+          fst
+            (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx)
+        in
+        (* Add the constructor name *)
+        fst (ctx_add_struct def ctx)
     | Enum variants ->
         fst
           (ctx_add_variants def
-- 
cgit v1.2.3