From fb6fdfd0c57de1ce16fb6bc373d5593c9446b0bb Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 4 May 2022 14:13:20 +0200
Subject: Make progress updating the code

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

(limited to 'src/ExtractToFStar.ml')

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 068448e9..4baa1fd6 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -1368,8 +1368,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     if has_decreases_clause then (
       F.pp_print_string fmt "Tot";
       F.pp_print_space fmt ());
-    extract_ty ctx fmt has_decreases_clause
-      (Collections.List.to_cons_nil def.signature.outputs);
+    extract_ty ctx fmt has_decreases_clause def.signature.output;
     (* Close the box for the return type *)
     F.pp_close_box fmt ();
     (* Print the decrease clause - rk.: a function with a decreases clause
@@ -1476,7 +1475,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
   if
     sg.type_params = []
     && (sg.inputs = [ mk_unit_ty ] || sg.inputs = [])
-    && sg.outputs = [ mk_result_ty mk_unit_ty ]
+    && sg.output = mk_result_ty mk_unit_ty
   then (
     (* Add a break before *)
     F.pp_print_break fmt 0 0;
-- 
cgit v1.2.3