Regenerate the files and fix the proofs

6 files changed, 180 insertions, 143 deletions

diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index 884d1778..a0658206 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -23,11 +23,11 @@ let x2_c : u32 = eval_global x2_body
 
 (** [constants::incr] *)
 let incr_fwd (n : u32) : result u32 =
-  begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end
+  begin match u32_add n 1 with | Fail e -> Fail e | Return i -> Return i end
 
 (** [constants::X3] *)
 let x3_body : result u32 =
-  begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end
+  begin match incr_fwd 32 with | Fail e -> Fail e | Return i -> Return i end
 let x3_c : u32 = eval_global x3_body
 
 (** [constants::mk_pair0] *)
@@ -42,12 +42,18 @@ let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
 
 (** [constants::P0] *)
 let p0_body : result (u32 & u32) =
-  begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+  begin match mk_pair0_fwd 0 1 with
+  | Fail e -> Fail e
+  | Return p -> Return p
+  end
 let p0_c : (u32 & u32) = eval_global p0_body
 
 (** [constants::P1] *)
 let p1_body : result (pair_t u32 u32) =
-  begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+  begin match mk_pair1_fwd 0 1 with
+  | Fail e -> Fail e
+  | Return p -> Return p
+  end
 let p1_c : pair_t u32 u32 = eval_global p1_body
 
 (** [constants::P2] *)
@@ -67,7 +73,10 @@ let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
 
 (** [constants::Y] *)
 let y_body : result (wrap_t i32) =
-  begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end
+  begin match wrap_new_fwd i32 2 with
+  | Fail e -> Fail e
+  | Return w -> Return w
+  end
 let y_c : wrap_t i32 = eval_global y_body
 
 (** [constants::unwrap_y] *)
@@ -75,7 +84,7 @@ let unwrap_y_fwd : result i32 = Return y_c.wrap_val
 
 (** [constants::YVAL] *)
 let yval_body : result i32 =
-  begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end
+  begin match unwrap_y_fwd with | Fail e -> Fail e | Return i -> Return i end
 let yval_c : i32 = eval_global yval_body
 
 (** [constants::get_z1::Z1] *)
@@ -87,7 +96,7 @@ let get_z1_fwd : result i32 = Return get_z1_z1_c
 
 (** [constants::add] *)
 let add_fwd (a : i32) (b : i32) : result i32 =
-  begin match i32_add a b with | Fail -> Fail | Return i -> Return i end
+  begin match i32_add a b with | Fail e -> Fail e | Return i -> Return i end
 
 (** [constants::Q1] *)
 let q1_body : result i32 = Return 5
@@ -99,19 +108,19 @@ let q2_c : i32 = eval_global q2_body
 
 (** [constants::Q3] *)
 let q3_body : result i32 =
-  begin match add_fwd q2_c 3 with | Fail -> Fail | Return i -> Return i end
+  begin match add_fwd q2_c 3 with | Fail e -> Fail e | Return i -> Return i end
 let q3_c : i32 = eval_global q3_body
 
 (** [constants::get_z2] *)
 let get_z2_fwd : result i32 =
   begin match get_z1_fwd with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return i ->
     begin match add_fwd i q3_c with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i0 ->
       begin match add_fwd q1_c i0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i1 -> Return i1
       end
     end
@@ -123,7 +132,7 @@ let s1_c : u32 = eval_global s1_body
 
 (** [constants::S2] *)
 let s2_body : result u32 =
-  begin match incr_fwd s1_c with | Fail -> Fail | Return i -> Return i end
+  begin match incr_fwd s1_c with | Fail e -> Fail e | Return i -> Return i end
 let s2_c : u32 = eval_global s2_body
 
 (** [constants::S3] *)
@@ -132,6 +141,9 @@ let s3_c : pair_t u32 u32 = eval_global s3_body
 
 (** [constants::S4] *)
 let s4_body : result (pair_t u32 u32) =
-  begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end
+  begin match mk_pair1_fwd 7 8 with
+  | Fail e -> Fail e
+  | Return p -> Return p
+  end
 let s4_c : pair_t u32 u32 = eval_global s4_body
 
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 68a0061e..a57472d4 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -10,13 +10,13 @@ include External.Opaque
 (** [external::swap] *)
 let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) =
   begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match core_mem_swap_back0 t x y st st0 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, _) ->
       begin match core_mem_swap_back1 t x y st st1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (st2, _) -> Return (st2, ())
       end
     end
@@ -28,13 +28,13 @@ let swap_back
   result (state & (t & t))
   =
   begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, _) ->
     begin match core_mem_swap_back0 t x y st st1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st2, x0) ->
       begin match core_mem_swap_back1 t x y st st2 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (_, y0) -> Return (st0, (x0, y0))
       end
     end
@@ -44,12 +44,12 @@ let swap_back
 let test_new_non_zero_u32_fwd
   (x : u32) (st : state) : result (state & core_num_nonzero_non_zero_u32_t) =
   begin match core_num_nonzero_non_zero_u32_new_fwd x st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, opt) ->
     begin match
       core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
       with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, nzu) -> Return (st1, nzu)
     end
   end
@@ -58,7 +58,7 @@ let test_new_non_zero_u32_fwd
 let test_vec_fwd : result unit =
   let v = vec_new u32 in
   begin match vec_push_back u32 v 0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return _ -> Return ()
   end
 
@@ -69,13 +69,13 @@ let _ = assert_norm (test_vec_fwd = Return ())
 let custom_swap_fwd
   (t : Type0) (x : t) (y : t) (st : state) : result (state & t) =
   begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match core_mem_swap_back0 t x y st st0 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, x0) ->
       begin match core_mem_swap_back1 t x y st st1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (st2, _) -> Return (st2, x0)
       end
     end
@@ -87,13 +87,13 @@ let custom_swap_back
   result (state & (t & t))
   =
   begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, _) ->
     begin match core_mem_swap_back0 t x y st st1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st2, _) ->
       begin match core_mem_swap_back1 t x y st st2 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (_, y0) -> Return (st0, (ret, y0))
       end
     end
@@ -103,7 +103,7 @@ let custom_swap_back
 let test_custom_swap_fwd
   (x : u32) (y : u32) (st : state) : result (state & unit) =
   begin match custom_swap_fwd u32 x y st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) -> Return (st0, ())
   end
 
@@ -113,18 +113,19 @@ let test_custom_swap_back
   result (state & (u32 & u32))
   =
   begin match custom_swap_back u32 x y st 1 st0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, (x0, y0)) -> Return (st1, (x0, y0))
   end
 
 (** [external::test_swap_non_zero] *)
 let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
   begin match swap_fwd u32 x 0 st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match swap_back u32 x 0 st st0 with
-    | Fail -> Fail
-    | Return (st1, (x0, _)) -> if x0 = 0 then Fail else Return (st1, x0)
+    | Fail e -> Fail e
+    | Return (st1, (x0, _)) ->
+      if x0 = 0 then Fail Failure else Return (st1, x0)
     end
   end
 
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 36dea95b..8424a7cc 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -32,38 +32,38 @@ type sum_t (t1 t2 : Type0) =
 
 (** [no_nested_borrows::neg_test] *)
 let neg_test_fwd (x : i32) : result i32 =
-  begin match i32_neg x with | Fail -> Fail | Return i -> Return i end
+  begin match i32_neg x with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::add_test] *)
 let add_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_add x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_add x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::subs_test] *)
 let subs_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_sub x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_sub x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::div_test] *)
 let div_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_div x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_div x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::div_test1] *)
 let div_test1_fwd (x : u32) : result u32 =
-  begin match u32_div x 2 with | Fail -> Fail | Return i -> Return i end
+  begin match u32_div x 2 with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::rem_test] *)
 let rem_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_rem x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_rem x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::cast_test] *)
 let cast_test_fwd (x : u32) : result i32 =
   begin match scalar_cast U32 I32 x with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return i -> Return i
   end
 
 (** [no_nested_borrows::test2] *)
 let test2_fwd : result unit =
-  begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end
+  begin match u32_add 23 44 with | Fail e -> Fail e | Return _ -> Return () end
 
 (** Unit test for [no_nested_borrows::test2] *)
 let _ = assert_norm (test2_fwd = Return ())
@@ -75,14 +75,14 @@ let get_max_fwd (x : u32) (y : u32) : result u32 =
 (** [no_nested_borrows::test3] *)
 let test3_fwd : result unit =
   begin match get_max_fwd 4 3 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return x ->
     begin match get_max_fwd 10 11 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return y ->
       begin match u32_add x y with
-      | Fail -> Fail
-      | Return z -> if not (z = 15) then Fail else Return ()
+      | Fail e -> Fail e
+      | Return z -> if not (z = 15) then Fail Failure else Return ()
       end
     end
   end
@@ -93,15 +93,16 @@ let _ = assert_norm (test3_fwd = Return ())
 (** [no_nested_borrows::test_neg1] *)
 let test_neg1_fwd : result unit =
   begin match i32_neg 3 with
-  | Fail -> Fail
-  | Return y -> if not (y = -3) then Fail else Return ()
+  | Fail e -> Fail e
+  | Return y -> if not (y = -3) then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
 let _ = assert_norm (test_neg1_fwd = Return ())
 
 (** [no_nested_borrows::refs_test1] *)
-let refs_test1_fwd : result unit = if not (1 = 1) then Fail else Return ()
+let refs_test1_fwd : result unit =
+  if not (1 = 1) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::refs_test1] *)
 let _ = assert_norm (refs_test1_fwd = Return ())
@@ -109,11 +110,14 @@ let _ = assert_norm (refs_test1_fwd = Return ())
 (** [no_nested_borrows::refs_test2] *)
 let refs_test2_fwd : result unit =
   if not (2 = 2)
-  then Fail
+  then Fail Failure
   else
     if not (0 = 0)
-    then Fail
-    else if not (2 = 2) then Fail else if not (2 = 2) then Fail else Return ()
+    then Fail Failure
+    else
+      if not (2 = 2)
+      then Fail Failure
+      else if not (2 = 2) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::refs_test2] *)
 let _ = assert_norm (refs_test2_fwd = Return ())
@@ -126,7 +130,7 @@ let _ = assert_norm (test_list1_fwd = Return ())
 
 (** [no_nested_borrows::test_box1] *)
 let test_box1_fwd : result unit =
-  let b = 1 in let x = b in if not (x = 1) then Fail else Return ()
+  let b = 1 in let x = b in if not (x = 1) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_box1] *)
 let _ = assert_norm (test_box1_fwd = Return ())
@@ -136,16 +140,17 @@ let copy_int_fwd (x : i32) : result i32 = Return x
 
 (** [no_nested_borrows::test_unreachable] *)
 let test_unreachable_fwd (b : bool) : result unit =
-  if b then Fail else Return ()
+  if b then Fail Failure else Return ()
 
 (** [no_nested_borrows::test_panic] *)
-let test_panic_fwd (b : bool) : result unit = if b then Fail else Return ()
+let test_panic_fwd (b : bool) : result unit =
+  if b then Fail Failure else Return ()
 
 (** [no_nested_borrows::test_copy_int] *)
 let test_copy_int_fwd : result unit =
   begin match copy_int_fwd 0 with
-  | Fail -> Fail
-  | Return y -> if not (0 = y) then Fail else Return ()
+  | Fail e -> Fail e
+  | Return y -> if not (0 = y) then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_copy_int] *)
@@ -162,8 +167,8 @@ let is_cons_fwd (t : Type0) (l : list_t t) : result bool =
 let test_is_cons_fwd : result unit =
   let l = ListNil in
   begin match is_cons_fwd i32 (ListCons 0 l) with
-  | Fail -> Fail
-  | Return b -> if not b then Fail else Return ()
+  | Fail e -> Fail e
+  | Return b -> if not b then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -171,14 +176,18 @@ let _ = assert_norm (test_is_cons_fwd = Return ())
 
 (** [no_nested_borrows::split_list] *)
 let split_list_fwd (t : Type0) (l : list_t t) : result (t & (list_t t)) =
-  begin match l with | ListCons hd tl -> Return (hd, tl) | ListNil -> Fail end
+  begin match l with
+  | ListCons hd tl -> Return (hd, tl)
+  | ListNil -> Fail Failure
+  end
 
 (** [no_nested_borrows::test_split_list] *)
 let test_split_list_fwd : result unit =
   let l = ListNil in
   begin match split_list_fwd i32 (ListCons 0 l) with
-  | Fail -> Fail
-  | Return p -> let (hd, _) = p in if not (hd = 0) then Fail else Return ()
+  | Fail e -> Fail e
+  | Return p ->
+    let (hd, _) = p in if not (hd = 0) then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_split_list] *)
@@ -196,18 +205,20 @@ let choose_back
 (** [no_nested_borrows::choose_test] *)
 let choose_test_fwd : result unit =
   begin match choose_fwd i32 true 0 0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return z ->
     begin match i32_add z 1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return z0 ->
       if not (z0 = 1)
-      then Fail
+      then Fail Failure
       else
         begin match choose_back i32 true 0 0 z0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (x, y) ->
-          if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
+          if not (x = 1)
+          then Fail Failure
+          else if not (y = 0) then Fail Failure else Return ()
         end
     end
   end
@@ -233,9 +244,12 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
   begin match l with
   | ListCons x l1 ->
     begin match list_length_fwd t l1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i ->
-      begin match u32_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end
+      begin match u32_add 1 i with
+      | Fail e -> Fail e
+      | Return i0 -> Return i0
+      end
     end
   | ListNil -> Return 0
   end
@@ -248,14 +262,14 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
     then Return x
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_shared_fwd t tl i0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x0 -> Return x0
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [no_nested_borrows::list_nth_mut] *)
@@ -266,14 +280,14 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
     then Return x
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_mut_fwd t tl i0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x0 -> Return x0
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [no_nested_borrows::list_nth_mut] *)
@@ -285,14 +299,14 @@ let rec list_nth_mut_back
     then Return (ListCons ret tl)
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_mut_back t tl i0 ret with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return tl0 -> Return (ListCons x tl0)
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [no_nested_borrows::list_rev_aux] *)
@@ -301,7 +315,7 @@ let rec list_rev_aux_fwd
   begin match li with
   | ListCons hd tl ->
     begin match list_rev_aux_fwd t tl (ListCons hd lo) with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return l -> Return l
     end
   | ListNil -> Return lo
@@ -311,7 +325,7 @@ let rec list_rev_aux_fwd
 let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) =
   let li = mem_replace_fwd (list_t t) l ListNil in
   begin match list_rev_aux_fwd t li ListNil with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return l0 -> Return l0
   end
 
@@ -321,48 +335,48 @@ let test_list_functions_fwd : result unit =
   let l0 = ListCons 2 l in
   let l1 = ListCons 1 l0 in
   begin match list_length_fwd i32 (ListCons 0 l1) with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return i ->
     if not (i = 3)
-    then Fail
+    then Fail Failure
     else
       begin match list_nth_shared_fwd i32 (ListCons 0 l1) 0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         if not (i0 = 0)
-        then Fail
+        then Fail Failure
         else
           begin match list_nth_shared_fwd i32 (ListCons 0 l1) 1 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i1 ->
             if not (i1 = 1)
-            then Fail
+            then Fail Failure
             else
               begin match list_nth_shared_fwd i32 (ListCons 0 l1) 2 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return i2 ->
                 if not (i2 = 2)
-                then Fail
+                then Fail Failure
                 else
                   begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return ls ->
                     begin match list_nth_shared_fwd i32 ls 0 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return i3 ->
                       if not (i3 = 0)
-                      then Fail
+                      then Fail Failure
                       else
                         begin match list_nth_shared_fwd i32 ls 1 with
-                        | Fail -> Fail
+                        | Fail e -> Fail e
                         | Return i4 ->
                           if not (i4 = 3)
-                          then Fail
+                          then Fail Failure
                           else
                             begin match list_nth_shared_fwd i32 ls 2 with
-                            | Fail -> Fail
+                            | Fail e -> Fail e
                             | Return i5 ->
-                              if not (i5 = 2) then Fail else Return ()
+                              if not (i5 = 2) then Fail Failure else Return ()
                             end
                         end
                     end
@@ -449,31 +463,31 @@ let new_pair1_fwd : result (struct_with_pair_t u32 u32) =
 (** [no_nested_borrows::test_constants] *)
 let test_constants_fwd : result unit =
   begin match new_tuple1_fwd with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return swt ->
     let (i, _) = swt.struct_with_tuple_p in
     if not (i = 1)
-    then Fail
+    then Fail Failure
     else
       begin match new_tuple2_fwd with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return swt0 ->
         let (i0, _) = swt0.struct_with_tuple_p in
         if not (i0 = 1)
-        then Fail
+        then Fail Failure
         else
           begin match new_tuple3_fwd with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return swt1 ->
             let (i1, _) = swt1.struct_with_tuple_p in
             if not (i1 = 1)
-            then Fail
+            then Fail Failure
             else
               begin match new_pair1_fwd with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return swp ->
                 if not (swp.struct_with_pair_p.pair_x = 1)
-                then Fail
+                then Fail Failure
                 else Return ()
               end
           end
@@ -491,7 +505,8 @@ let _ = assert_norm (test_weird_borrows1_fwd = Return ())
 
 (** [no_nested_borrows::test_mem_replace] *)
 let test_mem_replace_fwd_back (px : u32) : result u32 =
-  let y = mem_replace_fwd u32 px 1 in if not (y = 0) then Fail else Return 2
+  let y = mem_replace_fwd u32 px 1 in
+  if not (y = 0) then Fail Failure else Return 2
 
 (** [no_nested_borrows::test_shared_borrow_bool1] *)
 let test_shared_borrow_bool1_fwd (b : bool) : result u32 =
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index 424889ef..0f8604d1 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -7,13 +7,13 @@ open Primitives
 
 (** [paper::ref_incr] *)
 let ref_incr_fwd_back (x : i32) : result i32 =
-  begin match i32_add x 1 with | Fail -> Fail | Return x0 -> Return x0 end
+  begin match i32_add x 1 with | Fail e -> Fail e | Return x0 -> Return x0 end
 
 (** [paper::test_incr] *)
 let test_incr_fwd : result unit =
   begin match ref_incr_fwd_back 0 with
-  | Fail -> Fail
-  | Return x -> if not (x = 1) then Fail else Return ()
+  | Fail e -> Fail e
+  | Return x -> if not (x = 1) then Fail Failure else Return ()
   end
 
 (** Unit test for [paper::test_incr] *)
@@ -31,18 +31,20 @@ let choose_back
 (** [paper::test_choose] *)
 let test_choose_fwd : result unit =
   begin match choose_fwd i32 true 0 0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return z ->
     begin match i32_add z 1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return z0 ->
       if not (z0 = 1)
-      then Fail
+      then Fail Failure
       else
         begin match choose_back i32 true 0 0 z0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (x, y) ->
-          if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
+          if not (x = 1)
+          then Fail Failure
+          else if not (y = 0) then Fail Failure else Return ()
         end
     end
   end
@@ -63,14 +65,14 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
     then Return x
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_mut_fwd t tl i0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x0 -> Return x0
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [paper::list_nth_mut] *)
@@ -82,14 +84,14 @@ let rec list_nth_mut_back
     then Return (ListCons ret tl)
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_mut_back t tl i0 ret with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return tl0 -> Return (ListCons x tl0)
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [paper::sum] *)
@@ -97,9 +99,12 @@ let rec sum_fwd (l : list_t i32) : result i32 =
   begin match l with
   | ListCons x tl ->
     begin match sum_fwd tl with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i ->
-      begin match i32_add x i with | Fail -> Fail | Return i0 -> Return i0 end
+      begin match i32_add x i with
+      | Fail e -> Fail e
+      | Return i0 -> Return i0
+      end
     end
   | ListNil -> Return 0
   end
@@ -110,17 +115,17 @@ let test_nth_fwd : result unit =
   let l0 = ListCons 3 l in
   let l1 = ListCons 2 l0 in
   begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return x ->
     begin match i32_add x 1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return x0 ->
       begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l2 ->
         begin match sum_fwd l2 with
-        | Fail -> Fail
-        | Return i -> if not (i = 7) then Fail else Return ()
+        | Fail e -> Fail e
+        | Return i -> if not (i = 7) then Fail Failure else Return ()
         end
       end
     end
@@ -133,13 +138,13 @@ let _ = assert_norm (test_nth_fwd = Return ())
 let call_choose_fwd (p : (u32 & u32)) : result u32 =
   let (px, py) = p in
   begin match choose_fwd u32 true px py with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return pz ->
     begin match u32_add pz 1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return pz0 ->
       begin match choose_back u32 true px py pz0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (px0, _) -> Return px0
       end
     end
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index 73e98884..158a5fc7 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -18,7 +18,7 @@ let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
     then Return (ListCons hd tl)
     else
       begin match get_list_at_x_fwd tl x with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l -> Return l
       end
   | ListNil -> Return ListNil
@@ -33,7 +33,7 @@ let rec get_list_at_x_back
     then Return ret
     else
       begin match get_list_at_x_back tl x ret with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return tl0 -> Return (ListCons hd tl0)
       end
   | ListNil -> Return ret
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index 96138e46..82622656 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -18,9 +18,13 @@ let rec list_update #a ls i x =
 #pop-options
 
 (*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
 type result (a : Type0) : Type0 =
 | Return : v:a -> result a
-| Fail : result a
+| Fail : e:error -> result a
 
 // Monadic bind and return.
 // Re-definining those allows us to customize the result of the monadic notations
@@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x
 let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
     match m with
     | Return x -> f x
-    | Fail -> Fail
+    | Fail e -> Fail e
 
 // Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
 
 // Normalize and unwrap a successful result (used for globals).
 let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
@@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int =
 type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
 
 let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
-  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
 
 let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
 
 let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (x / y) else Fail
+  if y <> 0 then mk_scalar ty (x / y) else Fail Failure
 
 /// The remainder operation
 let int_rem (x : int) (y : int{y <> 0}) : int =
@@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
 let _ = assert_norm(int_rem (-1) (-2) = -1)
 
 let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
 
 let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
   mk_scalar ty (x + y)
@@ -258,7 +262,7 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
   (requires True)
   (ensures (fun res ->
     match res with
-    | Fail -> True
+    | Fail e -> e == Failure
     | Return v' -> length v' = length v + 1)) =
   if length v < usize_max then begin
     (**) assert_norm(length [x] == 1);
@@ -266,22 +270,22 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
     (**) assert(length (append v [x]) = length v + 1);
     Return (append v [x])
     end
-  else Fail
+  else Fail Failure
 
 // The **forward** function shouldn't be used
 let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
-  if i < length v then Return (list_update v i x) else Fail
+  if i < length v then Return (list_update v i x) else Fail Failure
 
 // The **backward** function shouldn't be used
 let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 
 let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
-  if i < length v then Return (list_update v i nx) else Fail
+  if i < length v then Return (list_update v i nx) else Fail Failure