Make progress on the extraction

1 files changed, 9 insertions, 1 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index fe007d31..864d513f 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -529,7 +529,15 @@ let type_decl_kind_to_qualif (kind : decl_kind)
            *)
           Some "with"
       | (Assumed | Declared), None -> Some "Axiom"
-      | _ -> raise (Failure "Unexpected"))
+      | SingleNonRec, None ->
+          (* This is for traits *)
+          Some "Record"
+      | _ ->
+          raise
+            (Failure
+               ("Unexpected: (" ^ show_decl_kind kind ^ ", "
+               ^ Print.option_to_string show_type_decl_kind type_kind
+               ^ ")")))
   | Lean -> (
       match kind with
       | SingleNonRec ->