From a49f413c0e0de494c003c622f8483e8c37d2618a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jan 2022 10:08:59 +0100
Subject: Cleanup a bit

---
 src/SymbolicToPure.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index e0ee557a..a575e835 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -336,7 +336,7 @@ let rec translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
   (* A small helper for "leave" types *)
   let wrap ty = if inside_mut then Some ty else None in
   match ty with
-  | T.Adt (type_id, regions, tys) -> (
+  | T.Adt (type_id, _, tys) -> (
       match type_id with
       | T.AdtId _ | Assumed _ ->
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
@@ -633,7 +633,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (lc : V.aloan_content) :
       (* Ignore *)
       None
 
-and aborrow_content_to_consumed (ctx : bs_ctx) (bc : V.aborrow_content) :
+and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) :
     typed_rvalue option =
   match bc with
   | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
@@ -649,7 +649,6 @@ and aborrow_content_to_consumed (ctx : bs_ctx) (bc : V.aborrow_content) :
       None
 
 and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : typed_rvalue option =
-  let translate = aproj_to_consumed ctx in
   match aproj with
   | V.AEndedProjLoans (msv, []) ->
       (* The symbolic value was left unchanged *)
@@ -707,6 +706,7 @@ let rec typed_avalue_to_given_back (av : V.typed_avalue) (ctx : bs_ctx) :
       | T.Tuple ->
           (* Return *)
           let variant_id = adt_v.variant_id in
+          assert (variant_id = None);
           if field_values = [] then (ctx, None)
           else
             let value = LvTuple field_values in
-- 
cgit v1.2.3