Rename meta into span

2 files changed, 324 insertions, 324 deletions

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index f49d39d0..ef958d2c 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -30,7 +30,7 @@ let log = Logging.borrows_log
       loans. This is used to merge borrows with abstractions, to compute loop
       fixed points for instance.
 *)
-let end_borrow_get_borrow (meta : Meta.meta)
+let end_borrow_get_borrow (span : Meta.span)
     (allowed_abs : AbstractionId.id option) (allow_inner_loans : bool)
     (l : BorrowId.id) (ctx : eval_ctx) :
     ( eval_ctx * (AbstractionId.id option * g_borrow_content) option,
@@ -43,7 +43,7 @@ let end_borrow_get_borrow (meta : Meta.meta)
   in
   let set_replaced_bc (abs_id : AbstractionId.id option) (bc : g_borrow_content)
       =
-    sanity_check __FILE__ __LINE__ (Option.is_none !replaced_bc) meta;
+    sanity_check __FILE__ __LINE__ (Option.is_none !replaced_bc) span;
     replaced_bc := Some (abs_id, bc)
   in
   (* Raise an exception if:
@@ -146,12 +146,12 @@ let end_borrow_get_borrow (meta : Meta.meta)
             let av = super#visit_typed_avalue outer av in
             (* Reconstruct *)
             ALoan (ASharedLoan (bids, v, av))
-        | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan _
         (* The loan has ended, so no need to update the outer borrows *)
         | AIgnoredMutLoan _ (* Nothing special to do *)
         | AEndedIgnoredMutLoan
-            { given_back = _; child = _; given_back_meta = _ }
+            { given_back = _; child = _; given_back_span = _ }
         (* Nothing special to do *)
         | AIgnoredSharedLoan _ ->
             (* Nothing special to do *)
@@ -182,7 +182,7 @@ let end_borrow_get_borrow (meta : Meta.meta)
                * Also note that, as we are moving the borrowed value inside the
                * abstraction (and not really giving the value back to the context)
                * we do not insert {!AEndedMutBorrow} but rather {!ABottom} *)
-              craise __FILE__ __LINE__ meta "Unimplemented"
+              craise __FILE__ __LINE__ span "Unimplemented"
               (* ABottom *))
             else
               (* Update the outer borrows before diving into the child avalue *)
@@ -203,7 +203,7 @@ let end_borrow_get_borrow (meta : Meta.meta)
         | AIgnoredMutBorrow (_, _)
         | AEndedMutBorrow _
         | AEndedIgnoredMutBorrow
-            { given_back = _; child = _; given_back_meta = _ }
+            { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedBorrow ->
             (* Nothing special to do *)
             super#visit_ABorrow outer bc
@@ -217,7 +217,7 @@ let end_borrow_get_borrow (meta : Meta.meta)
               set_replaced_bc (fst outer) (Abstract bc);
               (* Update the value - note that we are necessarily in the second
                * of the two cases described above *)
-              let asb = remove_borrow_from_asb meta l asb in
+              let asb = remove_borrow_from_asb span l asb in
               ABorrow (AProjSharedBorrow asb))
             else (* Nothing special to do *)
               super#visit_ABorrow outer bc
@@ -225,8 +225,8 @@ let end_borrow_get_borrow (meta : Meta.meta)
       method! visit_abs outer abs =
         (* Update the outer abs *)
         let outer_abs, outer_borrows = outer in
-        sanity_check __FILE__ __LINE__ (Option.is_none outer_abs) meta;
-        sanity_check __FILE__ __LINE__ (Option.is_none outer_borrows) meta;
+        sanity_check __FILE__ __LINE__ (Option.is_none outer_abs) span;
+        sanity_check __FILE__ __LINE__ (Option.is_none outer_borrows) span;
         let outer = (Some abs.abs_id, None) in
         super#visit_abs outer abs
     end
@@ -246,27 +246,27 @@ let end_borrow_get_borrow (meta : Meta.meta)
     give the value back.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
+let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
     (nv : typed_value) (ctx : eval_ctx) : eval_ctx =
   (* Sanity check *)
   exec_assert __FILE__ __LINE__
     (not (loans_in_value nv))
-    meta "Can not end a borrow because the value to give back contains bottom";
+    span "Can not end a borrow because the value to give back contains bottom";
   exec_assert __FILE__ __LINE__
     (not (bottom_in_value ctx.ended_regions nv))
-    meta "Can not end a borrow because the value to give back contains bottom";
+    span "Can not end a borrow because the value to give back contains bottom";
   (* Debug *)
   log#ldebug
     (lazy
       ("give_back_value:\n- bid: " ^ BorrowId.to_string bid ^ "\n- value: "
-      ^ typed_value_to_string ~meta:(Some meta) ctx nv
+      ^ typed_value_to_string ~span:(Some span) ctx nv
       ^ "\n- context:\n"
-      ^ eval_ctx_to_string ~meta:(Some meta) ctx
+      ^ eval_ctx_to_string ~span:(Some span) ctx
       ^ "\n"));
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    sanity_check __FILE__ __LINE__ (not !replaced) meta;
+    sanity_check __FILE__ __LINE__ (not !replaced) span;
     replaced := true
   in
   (* Whenever giving back symbolic values, they shouldn't contain already ended regions *)
@@ -274,7 +274,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
   (* We sometimes need to reborrow values while giving a value back due: prepare that *)
   let allow_reborrows = true in
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config meta allow_reborrows
+    prepare_reborrows config span allow_reborrows
   in
   (* The visitor to give back the values *)
   let obj =
@@ -304,7 +304,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
               (* Sanity check *)
               let expected_ty = ty in
               if nv.ty <> expected_ty then
-                craise __FILE__ __LINE__ meta
+                craise __FILE__ __LINE__ span
                   ("Value given back doesn't have the proper type:\n\
                     - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
                  ^ ty_to_string ctx nv.ty);
@@ -338,10 +338,10 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
               match nv.value with
               | VSymbolic sv ->
                   let abs = Option.get opt_abs in
-                  (* Remember the given back value as a meta-value
+                  (* Remember the given back value as a span-value
                    * TODO: it is a bit annoying to have to deconstruct
                    * the value... Think about a more elegant way. *)
-                  let given_back_meta = as_symbolic meta nv.value in
+                  let given_back_span = as_symbolic span nv.value in
                   (* The loan projector *)
                   let given_back =
                     mk_aproj_loans_value_from_symbolic_value abs.regions sv
@@ -351,8 +351,8 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
                   (* Return *)
                   ABorrow
                     (AEndedIgnoredMutBorrow
-                       { given_back; child; given_back_meta })
-              | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+                       { given_back; child; given_back_span })
+              | _ -> craise __FILE__ __LINE__ span "Unreachable"
             else
               (* Continue exploring *)
               ABorrow (super#visit_AIgnoredMutBorrow opt_abs bid' child)
@@ -367,7 +367,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
         (* Preparing a bit *)
         let regions, ancestors_regions =
           match opt_abs with
-          | None -> craise __FILE__ __LINE__ meta "Unreachable"
+          | None -> craise __FILE__ __LINE__ span "Unreachable"
           | Some abs -> (abs.regions, abs.ancestors_regions)
         in
         (* Rk.: there is a small issue with the types of the aloan values.
@@ -384,23 +384,23 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
                * an ended loan *)
               (* Register the insertion *)
               set_replaced ();
-              (* Remember the given back value as a meta-value *)
-              let given_back_meta = nv in
+              (* Remember the given back value as a span-value *)
+              let given_back_span = nv in
               (* Apply the projection *)
               let given_back =
-                apply_proj_borrows meta check_symbolic_no_ended ctx
+                apply_proj_borrows span check_symbolic_no_ended ctx
                   fresh_reborrow regions ancestors_regions nv borrowed_value_aty
               in
               (* Continue giving back in the child value *)
               let child = super#visit_typed_avalue opt_abs child in
               (* Return the new value *)
-              ALoan (AEndedMutLoan { child; given_back; given_back_meta }))
+              ALoan (AEndedMutLoan { child; given_back; given_back_span }))
             else (* Continue exploring *)
               super#visit_ALoan opt_abs lc
         | ASharedLoan (_, _, _) ->
             (* We are giving back a value to a *mutable* loan: nothing special to do *)
             super#visit_ALoan opt_abs lc
-        | AEndedMutLoan { child = _; given_back = _; given_back_meta = _ }
+        | AEndedMutLoan { child = _; given_back = _; given_back_span = _ }
         | AEndedSharedLoan (_, _) ->
             (* Nothing special to do *)
             super#visit_ALoan opt_abs lc
@@ -408,23 +408,23 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
             (* This loan is ignored, but we may have to project on a subvalue
              * of the value which is given back *)
             if opt_bid = Some bid then
-              (* Remember the given back value as a meta-value *)
-              let given_back_meta = nv in
+              (* Remember the given back value as a span-value *)
+              let given_back_span = nv in
               (* Note that we replace the ignored mut loan by an *ended* ignored
                * mut loan. Also, this is not the loan we are looking for *per se*:
                * we don't register the fact that we inserted the value somewhere
                * (i.e., we don't call {!set_replaced}) *)
               let given_back =
-                apply_proj_borrows meta check_symbolic_no_ended ctx
+                apply_proj_borrows span check_symbolic_no_ended ctx
                   fresh_reborrow regions ancestors_regions nv borrowed_value_aty
               in
               (* Continue giving back in the child value *)
               let child = super#visit_typed_avalue opt_abs child in
               ALoan
-                (AEndedIgnoredMutLoan { given_back; child; given_back_meta })
+                (AEndedIgnoredMutLoan { given_back; child; given_back_span })
             else super#visit_ALoan opt_abs lc
         | AEndedIgnoredMutLoan
-            { given_back = _; child = _; given_back_meta = _ }
+            { given_back = _; child = _; given_back_span = _ }
         | AIgnoredSharedLoan _ ->
             (* Nothing special to do *)
             super#visit_ALoan opt_abs lc
@@ -433,7 +433,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
         (* We remember in which abstraction we are before diving -
          * this is necessary for projecting values: we need to know
          * over which regions to project *)
-        sanity_check __FILE__ __LINE__ (Option.is_none opt_abs) meta;
+        sanity_check __FILE__ __LINE__ (Option.is_none opt_abs) span;
         super#visit_EAbs (Some abs) abs
     end
   in
@@ -441,19 +441,19 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert __FILE__ __LINE__ !replaced meta "No loan updated";
+  cassert __FILE__ __LINE__ !replaced span "No loan updated";
   (* Apply the reborrows *)
   apply_registered_reborrows ctx
 
 (** Give back a *modified* symbolic value. *)
-let give_back_symbolic_value (_config : config) (meta : Meta.meta)
+let give_back_symbolic_value (_config : config) (span : Meta.span)
     (proj_regions : RegionId.Set.t) (proj_ty : rty) (sv : symbolic_value)
     (nsv : symbolic_value) (ctx : eval_ctx) : eval_ctx =
   (* Sanity checks *)
   sanity_check __FILE__ __LINE__
     (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty)
-    meta;
-  (* Store the given-back value as a meta-value for synthesis purposes *)
+    span;
+  (* Store the given-back value as a span-value for synthesis purposes *)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
   let subst (_abs : abs) local_given_back =
@@ -474,11 +474,11 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta)
          type [T]! We thus *mustn't* introduce a projector here.
       *)
       (* AProjBorrows (nsv, sv.sv_ty) *)
-      internal_error __FILE__ __LINE__ meta
+      internal_error __FILE__ __LINE__ span
     in
     AProjLoans (sv, (mv, child_proj) :: local_given_back)
   in
-  update_intersecting_aproj_loans meta proj_regions proj_ty sv subst ctx
+  update_intersecting_aproj_loans span proj_regions proj_ty sv subst ctx
 
 (** Auxiliary function to end borrows. See {!give_back}.
 
@@ -493,13 +493,13 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta)
     end abstraction when ending this abstraction. When doing this, we need
     to convert the {!avalue} to a {!type:value} by introducing the proper symbolic values.
  *)
-let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
+let give_back_avalue_to_same_abstraction (_config : config) (span : Meta.span)
     (bid : BorrowId.id) (nv : typed_avalue) (nsv : typed_value) (ctx : eval_ctx)
     : eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    cassert __FILE__ __LINE__ (not !replaced) meta
+    cassert __FILE__ __LINE__ (not !replaced) span
       "Exacly one loan should be updated";
     replaced := true
   in
@@ -539,7 +539,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
                * {!typed_avalue} *)
               let _, expected_ty, _ = ty_get_ref ty in
               if nv.ty <> expected_ty then
-                craise __FILE__ __LINE__ meta
+                craise __FILE__ __LINE__ span
                   ("Value given back doesn't have the proper type:\n\
                     - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
                  ^ ty_to_string ctx nv.ty);
@@ -550,12 +550,12 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
               set_replaced ();
               (* Return the new value *)
               ALoan
-                (AEndedMutLoan { given_back = nv; child; given_back_meta = nsv }))
+                (AEndedMutLoan { given_back = nv; child; given_back_span = nsv }))
             else (* Continue exploring *)
               super#visit_ALoan opt_abs lc
         | ASharedLoan (_, _, _)
         (* We are giving back a value to a *mutable* loan: nothing special to do *)
-        | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _) ->
             (* Nothing special to do *)
             super#visit_ALoan opt_abs lc
@@ -568,13 +568,13 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
                * we don't register the fact that we inserted the value somewhere
                * (i.e., we don't call {!set_replaced}) *)
               (* Sanity check *)
-              sanity_check __FILE__ __LINE__ (nv.ty = ty) meta;
+              sanity_check __FILE__ __LINE__ (nv.ty = ty) span;
               ALoan
                 (AEndedIgnoredMutLoan
-                   { given_back = nv; child; given_back_meta = nsv }))
+                   { given_back = nv; child; given_back_span = nsv }))
             else super#visit_ALoan opt_abs lc
         | AEndedIgnoredMutLoan
-            { given_back = _; child = _; given_back_meta = _ }
+            { given_back = _; child = _; given_back_span = _ }
         | AIgnoredSharedLoan _ ->
             (* Nothing special to do *)
             super#visit_ALoan opt_abs lc
@@ -584,7 +584,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert __FILE__ __LINE__ !replaced meta "No loan updated";
+  cassert __FILE__ __LINE__ !replaced span "No loan updated";
   (* Return *)
   ctx
 
@@ -597,12 +597,12 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
     we update.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
+let give_back_shared _config (span : Meta.span) (bid : BorrowId.id)
     (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    cassert __FILE__ __LINE__ (not !replaced) meta
+    cassert __FILE__ __LINE__ (not !replaced) span
       "Exactly one loan should be updated";
     replaced := true
   in
@@ -650,14 +650,14 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
             else
               (* Not the loan we are looking for: continue exploring *)
               super#visit_ALoan opt_abs lc
-        | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         (* Nothing special to do (the loan has ended) *)
         | AEndedSharedLoan (_, _)
         (* Nothing special to do (the loan has ended) *)
         | AIgnoredMutLoan (_, _)
         (* Nothing special to do (we are giving back a *shared* borrow) *)
         | AEndedIgnoredMutLoan
-            { given_back = _; child = _; given_back_meta = _ }
+            { given_back = _; child = _; given_back_span = _ }
         (* Nothing special to do *)
         | AIgnoredSharedLoan _ ->
             (* Nothing special to do *)
@@ -668,7 +668,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert __FILE__ __LINE__ !replaced meta "No loan updated";
+  cassert __FILE__ __LINE__ !replaced span "No loan updated";
   (* Return *)
   ctx
 
@@ -677,12 +677,12 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
     to an environment by inserting a new borrow id in the set of borrows tracked
     by a shared value, referenced by the [original_bid] argument.
  *)
-let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id)
+let reborrow_shared (span : Meta.span) (original_bid : BorrowId.id)
     (new_bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
   (* Keep track of changes *)
   let r = ref false in
   let set_ref () =
-    sanity_check __FILE__ __LINE__ (not !r) meta;
+    sanity_check __FILE__ __LINE__ (not !r) span;
     r := true
   in
 
@@ -712,7 +712,7 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id)
 
   let env = obj#visit_env () ctx.env in
   (* Check that we reborrowed once *)
-  sanity_check __FILE__ __LINE__ !r meta;
+  sanity_check __FILE__ __LINE__ !r span;
   { ctx with env }
 
 (** Convert an {!type:avalue} to a {!type:value}.
@@ -731,9 +731,9 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id)
     be expanded (because expanding this symbolic value would require expanding
     a reference whose region has already ended).
  *)
-let convert_avalue_to_given_back_value (meta : Meta.meta) (av : typed_avalue) :
+let convert_avalue_to_given_back_value (span : Meta.span) (av : typed_avalue) :
     symbolic_value =
-  mk_fresh_symbolic_value meta av.ty
+  mk_fresh_symbolic_value span av.ty
 
 (** Auxiliary function: see {!end_borrow_aux}.
 
@@ -751,19 +751,19 @@ let convert_avalue_to_given_back_value (meta : Meta.meta) (av : typed_avalue) :
     borrows. This kind of internal reshuffling. should be similar to ending
     abstractions (it is tantamount to ending *sub*-abstractions).
  *)
-let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id)
+let give_back (config : config) (span : Meta.span) (l : BorrowId.id)
     (bc : g_borrow_content) (ctx : eval_ctx) : eval_ctx =
   (* Debug *)
   log#ldebug
     (lazy
       (let bc =
          match bc with
-         | Concrete bc -> borrow_content_to_string ~meta:(Some meta) ctx bc
-         | Abstract bc -> aborrow_content_to_string ~meta:(Some meta) ctx bc
+         | Concrete bc -> borrow_content_to_string ~span:(Some span) ctx bc
+         | Abstract bc -> aborrow_content_to_string ~span:(Some span) ctx bc
        in
        "give_back:\n- bid: " ^ BorrowId.to_string l ^ "\n- content: " ^ bc
        ^ "\n- context:\n"
-       ^ eval_ctx_to_string ~meta:(Some meta) ctx
+       ^ eval_ctx_to_string ~span:(Some span) ctx
        ^ "\n"));
   (* This is used for sanity checks *)
   let sanity_ek =
@@ -772,60 +772,60 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id)
   match bc with
   | Concrete (VMutBorrow (l', tv)) ->
       (* Sanity check *)
-      sanity_check __FILE__ __LINE__ (l' = l) meta;
-      sanity_check __FILE__ __LINE__ (not (loans_in_value tv)) meta;
+      sanity_check __FILE__ __LINE__ (l' = l) span;
+      sanity_check __FILE__ __LINE__ (not (loans_in_value tv)) span;
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
       sanity_check __FILE__ __LINE__
-        (Option.is_some (lookup_loan_opt meta sanity_ek l ctx))
-        meta;
+        (Option.is_some (lookup_loan_opt span sanity_ek l ctx))
+        span;
       (* Update the context *)
-      give_back_value config meta l tv ctx
+      give_back_value config span l tv ctx
   | Concrete (VSharedBorrow l' | VReservedMutBorrow l') ->
       (* Sanity check *)
-      sanity_check __FILE__ __LINE__ (l' = l) meta;
+      sanity_check __FILE__ __LINE__ (l' = l) span;
       (* Check that the borrow is somewhere - purely a sanity check *)
       sanity_check __FILE__ __LINE__
-        (Option.is_some (lookup_loan_opt meta sanity_ek l ctx))
-        meta;
+        (Option.is_some (lookup_loan_opt span sanity_ek l ctx))
+        span;
       (* Update the context *)
-      give_back_shared config meta l ctx
+      give_back_shared config span l ctx
   | Abstract (AMutBorrow (l', av)) ->
       (* Sanity check *)
-      sanity_check __FILE__ __LINE__ (l' = l) meta;
+      sanity_check __FILE__ __LINE__ (l' = l) span;
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
       sanity_check __FILE__ __LINE__
-        (Option.is_some (lookup_loan_opt meta sanity_ek l ctx))
-        meta;
+        (Option.is_some (lookup_loan_opt span sanity_ek l ctx))
+        span;
       (* Convert the avalue to a (fresh symbolic) value.
 
          Rem.: we shouldn't do this here. We should do this in a function
          which takes care of ending *sub*-abstractions.
       *)
-      let sv = convert_avalue_to_given_back_value meta av in
+      let sv = convert_avalue_to_given_back_value span av in
       (* Update the context *)
-      give_back_avalue_to_same_abstraction config meta l av
+      give_back_avalue_to_same_abstraction config span l av
         (mk_typed_value_from_symbolic_value sv)
         ctx
   | Abstract (ASharedBorrow l') ->
       (* Sanity check *)
-      sanity_check __FILE__ __LINE__ (l' = l) meta;
+      sanity_check __FILE__ __LINE__ (l' = l) span;
       (* Check that the borrow is somewhere - purely a sanity check *)
       sanity_check __FILE__ __LINE__
-        (Option.is_some (lookup_loan_opt meta sanity_ek l ctx))
-        meta;
+        (Option.is_some (lookup_loan_opt span sanity_ek l ctx))
+        span;
       (* Update the context *)
-      give_back_shared config meta l ctx
+      give_back_shared config span l ctx
   | Abstract (AProjSharedBorrow asb) ->
       (* Sanity check *)
-      sanity_check __FILE__ __LINE__ (borrow_in_asb l asb) meta;
+      sanity_check __FILE__ __LINE__ (borrow_in_asb l asb) span;
       (* Update the context *)
-      give_back_shared config meta l ctx
+      give_back_shared config span l ctx
   | Abstract
       ( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _
       | AEndedSharedBorrow ) ->
-      craise __FILE__ __LINE__ meta "Unreachable"
+      craise __FILE__ __LINE__ span "Unreachable"
 
-let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
+let check_borrow_disappeared (span : Meta.span) (fun_name : string)
     (l : BorrowId.id) (ctx0 : eval_ctx) (ctx : eval_ctx) : unit =
   (match lookup_borrow_opt ek_all l ctx with
   | None -> () (* Ok *)
@@ -834,21 +834,21 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
         (lazy
           (fun_name ^ ": " ^ BorrowId.to_string l
          ^ ": borrow didn't disappear:\n- original context:\n"
-          ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+          ^ eval_ctx_to_string ~span:(Some span) ctx0
           ^ "\n\n- new context:\n"
-          ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-      internal_error __FILE__ __LINE__ meta);
-  match lookup_loan_opt meta ek_all l ctx with
+          ^ eval_ctx_to_string ~span:(Some span) ctx));
+      internal_error __FILE__ __LINE__ span);
+  match lookup_loan_opt span ek_all l ctx with
   | None -> () (* Ok *)
   | Some _ ->
       log#ltrace
         (lazy
           (fun_name ^ ": " ^ BorrowId.to_string l
          ^ ": loan didn't disappear:\n- original context:\n"
-          ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+          ^ eval_ctx_to_string ~span:(Some span) ctx0
           ^ "\n\n- new context:\n"
-          ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-      internal_error __FILE__ __LINE__ meta
+          ^ eval_ctx_to_string ~span:(Some span) ctx));
+      internal_error __FILE__ __LINE__ span
 
 (** End a borrow identified by its borrow id in a context.
 
@@ -871,27 +871,27 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
     perform anything smart and is trusted, and another function for the
     book-keeping.
  *)
-let rec end_borrow_aux (config : config) (meta : Meta.meta)
+let rec end_borrow_aux (config : config) (span : Meta.span)
     (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option)
     (l : BorrowId.id) : cm_fun =
  fun ctx ->
   (* Check that we don't loop *)
   let chain0 = chain in
   let chain =
-    add_borrow_or_abs_id_to_chain meta "end_borrow_aux: " (BorrowId l) chain
+    add_borrow_or_abs_id_to_chain span "end_borrow_aux: " (BorrowId l) chain
   in
   log#ldebug
     (lazy
       ("end borrow: " ^ BorrowId.to_string l ^ ":\n- original context:\n"
-      ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+      ^ eval_ctx_to_string ~span:(Some span) ctx));
 
   (* Utility function for the sanity checks: check that the borrow disappeared
    * from the context *)
   let ctx0 = ctx in
-  let check = check_borrow_disappeared meta "end borrow" l ctx0 in
+  let check = check_borrow_disappeared span "end borrow" l ctx0 in
   (* Start by ending the borrow itself (we lookup it up and replace it with [Bottom] *)
   let allow_inner_loans = false in
-  match end_borrow_get_borrow meta allowed_abs allow_inner_loans l ctx with
+  match end_borrow_get_borrow span allowed_abs allow_inner_loans l ctx with
   (* Two cases:
      - error: we found outer borrows (the borrow is inside a borrowed value) or
        inner loans (the borrow contains loans)
@@ -921,11 +921,11 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta)
           let allowed_abs' = None in
           (* End the outer borrows *)
           let ctx, cc =
-            end_borrows_aux config meta chain allowed_abs' bids ctx
+            end_borrows_aux config span chain allowed_abs' bids ctx
           in
           (* Retry to end the borrow *)
           let ctx, cc =
-            comp cc (end_borrow_aux config meta chain0 allowed_abs l ctx)
+            comp cc (end_borrow_aux config span chain0 allowed_abs l ctx)
           in
           (* Check and continue *)
           check ctx;
@@ -933,17 +933,17 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta)
       | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) ->
           let allowed_abs' = None in
           (* End the outer borrow *)
-          let ctx, cc = end_borrow_aux config meta chain allowed_abs' bid ctx in
+          let ctx, cc = end_borrow_aux config span chain allowed_abs' bid ctx in
           (* Retry to end the borrow *)
           let ctx, cc =
-            comp cc (end_borrow_aux config meta chain0 allowed_abs l ctx)
+            comp cc (end_borrow_aux config span chain0 allowed_abs l ctx)
           in
           (* Check and continue *)
           check ctx;
           (ctx, cc)
       | OuterAbs abs_id ->
           (* The borrow is inside an abstraction: end the whole abstraction *)
-          let ctx, end_abs = end_abstraction_aux config meta chain abs_id ctx in
+          let ctx, end_abs = end_abstraction_aux config span chain abs_id ctx in
           (* Sanity check *)
           check ctx;
           (ctx, end_abs))
@@ -951,7 +951,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta)
       log#ldebug (lazy "End borrow: borrow not found");
       (* It is possible that we can't find a borrow in symbolic mode (ending
        * an abstraction may end several borrows at once *)
-      sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta;
+      sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) span;
       (* Do a sanity check and continue *)
       check ctx;
       (ctx, fun e -> e)
@@ -963,10 +963,10 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta)
       | Concrete (VMutBorrow (_, bv)) ->
           sanity_check __FILE__ __LINE__
             (Option.is_none (get_first_loan_in_value bv))
-            meta
+            span
       | _ -> ());
       (* Give back the value *)
-      let ctx = give_back config meta l bc ctx in
+      let ctx = give_back config span l bc ctx in
       (* Do a sanity check and continue *)
       check ctx;
       (* Save a snapshot of the environment for the name generation *)
@@ -974,7 +974,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta)
       (* Compose *)
       (ctx, cc)
 
-and end_borrows_aux (config : config) (meta : Meta.meta)
+and end_borrows_aux (config : config) (span : Meta.span)
     (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option)
     (lset : BorrowId.Set.t) : cm_fun =
  fun ctx ->
@@ -983,15 +983,15 @@ and end_borrows_aux (config : config) (meta : Meta.meta)
      a matter of taste, and may make debugging easier *)
   let ids = BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in
   fold_left_apply_continuation
-    (fun id ctx -> end_borrow_aux config meta chain allowed_abs id ctx)
+    (fun id ctx -> end_borrow_aux config span chain allowed_abs id ctx)
     ids ctx
 
-and end_abstraction_aux (config : config) (meta : Meta.meta)
+and end_abstraction_aux (config : config) (span : Meta.span)
     (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun =
  fun ctx ->
   (* Check that we don't loop *)
   let chain =
-    add_borrow_or_abs_id_to_chain meta "end_abstraction_aux: " (AbsId abs_id)
+    add_borrow_or_abs_id_to_chain span "end_abstraction_aux: " (AbsId abs_id)
       chain
   in
   (* Remember the original context for printing purposes *)
@@ -1001,7 +1001,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta)
       ("end_abstraction_aux: "
       ^ AbstractionId.to_string abs_id
       ^ "\n- original context:\n"
-      ^ eval_ctx_to_string ~meta:(Some meta) ctx0));
+      ^ eval_ctx_to_string ~span:(Some span) ctx0));
 
   (* Lookup the abstraction - note that if we end a list of abstractions,
      ending one abstraction may lead to the current abstraction having
@@ -1019,34 +1019,34 @@ and end_abstraction_aux (config : config) (meta : Meta.meta)
       (* Check that we can end the abstraction *)
       if abs.can_end then ()
       else
-        craise __FILE__ __LINE__ meta
+        craise __FILE__ __LINE__ span
           ("Can't end abstraction "
           ^ AbstractionId.to_string abs.abs_id
           ^ " as it is set as non-endable");
 
       (* End the parent abstractions first *)
-      let ctx, cc = end_abstractions_aux config meta chain abs.parents ctx in
+      let ctx, cc = end_abstractions_aux config span chain abs.parents ctx in
       log#ldebug
         (lazy
           ("end_abstraction_aux: "
           ^ AbstractionId.to_string abs_id
           ^ "\n- context after parent abstractions ended:\n"
-          ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+          ^ eval_ctx_to_string ~span:(Some span) ctx));
 
       (* End the loans inside the abstraction *)
       let ctx, cc =
-        comp cc (end_abstraction_loans config meta chain abs_id ctx)
+        comp cc (end_abstraction_loans config span chain abs_id ctx)
       in
       log#ldebug
         (lazy
           ("end_abstraction_aux: "
           ^ AbstractionId.to_string abs_id
           ^ "\n- context after loans ended:\n"
-          ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+          ^ eval_ctx_to_string ~span:(Some span) ctx));
 
       (* End the abstraction itself by redistributing the borrows it contains *)
       let ctx, cc =
-        comp cc (end_abstraction_borrows config meta chain abs_id ctx)
+        comp cc (end_abstraction_borrows config span chain abs_id ctx)
       in
 
       (* End the regions owned by the abstraction - note that we don't need to
@@ -1061,7 +1061,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta)
          the abstraction itself.
          **Rk.**: this is where we synthesize the updated symbolic AST *)
       let ctx, cc =
-        comp cc (end_abstraction_remove_from_context config meta abs_id ctx)
+        comp cc (end_abstraction_remove_from_context config span abs_id ctx)
       in
 
       (* Debugging *)
@@ -1070,12 +1070,12 @@ and end_abstraction_aux (config : config) (meta : Meta.meta)
           ("end_abstraction_aux: "
           ^ AbstractionId.to_string abs_id
           ^ "\n- original context:\n"
-          ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+          ^ eval_ctx_to_string ~span:(Some span) ctx0
           ^ "\n\n- new context:\n"
-          ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+          ^ eval_ctx_to_string ~span:(Some span) ctx));
 
       (* Sanity check: ending an abstraction must preserve the invariants *)
-      Invariants.check_invariants meta ctx;
+      Invariants.check_invariants span ctx;
 
       (* Save a snapshot of the environment for the name generation *)
       let cc = cc_comp cc (SynthesizeSymbolic.save_snapshot ctx) in
@@ -1083,7 +1083,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta)
       (* Return *)
       (ctx, cc)
 
-and end_abstractions_aux (config : config) (meta : Meta.meta)
+and end_abstractions_aux (config : config) (span : Meta.span)
     (chain : borrow_or_abs_ids) (abs_ids : AbstractionId.Set.t) : cm_fun =
  fun ctx ->
   (* This is not necessary, but we prefer to reorder the abstraction ids,
@@ -1091,10 +1091,10 @@ and end_abstractions_aux (config : config) (meta : Meta.meta)
    * a matter of taste, and may make debugging easier *)
   let abs_ids = AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in
   fold_left_apply_continuation
-    (fun id ctx -> end_abstraction_aux config meta chain id ctx)
+    (fun id ctx -> end_abstraction_aux config span chain id ctx)
     abs_ids ctx
 
-and end_abstraction_loans (config : config) (meta : Meta.meta)
+and end_abstraction_loans (config : config) (span : Meta.span)
     (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun =
  fun ctx ->
   (* Lookup the abstraction *)
@@ -1103,7 +1103,7 @@ and end_abstraction_loans (config : config) (meta : Meta.meta)
    *
    * We ignore the "ignored mut/shared loans": as we should have already ended
    * the parent abstractions, they necessarily come from children. *)
-  let opt_loan = get_first_non_ignored_aloan_in_abstraction meta abs in
+  let opt_loan = get_first_non_ignored_aloan_in_abstraction span abs in
   match opt_loan with
   | None ->
       (* No loans: nothing to update *)
@@ -1112,21 +1112,21 @@ and end_abstraction_loans (config : config) (meta : Meta.meta)
       (* There are loans: end the corresponding borrows, then recheck *)
       let ctx, cc =
         match bids with
-        | Borrow bid -> end_borrow_aux config meta chain None bid ctx
-        | Borrows bids -> end_borrows_aux config meta chain None bids ctx
+        | Borrow bid -> end_borrow_aux config span chain None bid ctx
+        | Borrows bids -> end_borrows_aux config span chain None bids ctx
       in
       (* Reexplore, looking for loans *)
-      comp cc (end_abstraction_loans config meta chain abs_id ctx)
+      comp cc (end_abstraction_loans config span chain abs_id ctx)
   | Some (SymbolicValue sv) ->
       (* There is a proj_loans over a symbolic value: end the proj_borrows
          which intersect this proj_loans, then end the proj_loans itself *)
       let ctx, cc =
-        end_proj_loans_symbolic config meta chain abs_id abs.regions sv ctx
+        end_proj_loans_symbolic config span chain abs_id abs.regions sv ctx
       in
       (* Reexplore, looking for loans *)
-      comp cc (end_abstraction_loans config meta chain abs_id ctx)
+      comp cc (end_abstraction_loans config span chain abs_id ctx)
 
-and end_abstraction_borrows (config : config) (meta : Meta.meta)
+and end_abstraction_borrows (config : config) (span : Meta.span)
     (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun =
  fun ctx ->
   log#ldebug
@@ -1177,7 +1177,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta)
 
       method! visit_aproj env sproj =
         (match sproj with
-        | AProjLoans _ -> craise __FILE__ __LINE__ meta "Unexpected"
+        | AProjLoans _ -> craise __FILE__ __LINE__ span "Unexpected"
         | AProjBorrows (sv, proj_ty) -> raise (FoundAProjBorrows (sv, proj_ty))
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj env sproj
@@ -1186,7 +1186,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta)
       method! visit_borrow_content _ bc =
         match bc with
         | VSharedBorrow _ | VMutBorrow (_, _) -> raise (FoundBorrowContent bc)
-        | VReservedMutBorrow _ -> craise __FILE__ __LINE__ meta "Unreachable"
+        | VReservedMutBorrow _ -> craise __FILE__ __LINE__ span "Unreachable"
     end
   in
   (* Lookup the abstraction *)
@@ -1202,25 +1202,25 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta)
       log#ldebug
         (lazy
           ("end_abstraction_borrows: found aborrow content: "
-          ^ aborrow_content_to_string ~meta:(Some meta) ctx bc));
+          ^ aborrow_content_to_string ~span:(Some span) ctx bc));
       let ctx =
         match bc with
         | AMutBorrow (bid, av) ->
             (* First, convert the avalue to a (fresh symbolic) value *)
-            let sv = convert_avalue_to_given_back_value meta av in
+            let sv = convert_avalue_to_given_back_value span av in
             (* Replace the mut borrow to register the fact that we ended
              * it and store with it the freshly generated given back value *)
             let ended_borrow = ABorrow (AEndedMutBorrow (sv, av)) in
-            let ctx = update_aborrow meta ek_all bid ended_borrow ctx in
+            let ctx = update_aborrow span ek_all bid ended_borrow ctx in
             (* Give the value back *)
             let sv = mk_typed_value_from_symbolic_value sv in
-            give_back_value config meta bid sv ctx
+            give_back_value config span bid sv ctx
         | ASharedBorrow bid ->
             (* Replace the shared borrow to account for the fact it ended *)
             let ended_borrow = ABorrow AEndedSharedBorrow in
-            let ctx = update_aborrow meta ek_all bid ended_borrow ctx in
+            let ctx = update_aborrow span ek_all bid ended_borrow ctx in
             (* Give back *)
-            give_back_shared config meta bid ctx
+            give_back_shared config span bid ctx
         | AProjSharedBorrow asb ->
             (* Retrieve the borrow ids *)
             let bids =
@@ -1235,21 +1235,21 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta)
              * can use to identify the whole set *)
             let repr_bid = List.hd bids in
             (* Replace the shared borrow with Bottom *)
-            let ctx = update_aborrow meta ek_all repr_bid ABottom ctx in
+            let ctx = update_aborrow span ek_all repr_bid ABottom ctx in
             (* Give back the shared borrows *)
             let ctx =
               List.fold_left
-                (fun ctx bid -> give_back_shared config meta bid ctx)
+                (fun ctx bid -> give_back_shared config span bid ctx)
                 ctx bids
             in
             (* Continue *)
             ctx
         | AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _
         | AEndedSharedBorrow ->
-            craise __FILE__ __LINE__ meta "Unexpected"
+            craise __FILE__ __LINE__ span "Unexpected"
       in
       (* Reexplore *)
-      end_abstraction_borrows config meta chain abs_id ctx
+      end_abstraction_borrows config span chain abs_id ctx
   (* There are symbolic borrows: end them, then reexplore *)
   | FoundAProjBorrows (sv, proj_ty) ->
       log#ldebug
@@ -1257,55 +1257,55 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta)
           ("end_abstraction_borrows: found aproj borrows: "
           ^ aproj_to_string ctx (AProjBorrows (sv, proj_ty))));
       (* Generate a fresh symbolic value *)
-      let nsv = mk_fresh_symbolic_value meta proj_ty in
+      let nsv = mk_fresh_symbolic_value span proj_ty in
       (* Replace the proj_borrows - there should be exactly one *)
       let ended_borrow = AEndedProjBorrows nsv in
-      let ctx = update_aproj_borrows meta abs.abs_id sv ended_borrow ctx in
+      let ctx = update_aproj_borrows span abs.abs_id sv ended_borrow ctx in
       (* Give back the symbolic value *)
       let ctx =
-        give_back_symbolic_value config meta abs.regions proj_ty sv nsv ctx
+        give_back_symbolic_value config span abs.regions proj_ty sv nsv ctx
       in
       (* Reexplore *)
-      end_abstraction_borrows config meta chain abs_id ctx
+      end_abstraction_borrows config span chain abs_id ctx
   (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *)
   | FoundBorrowContent bc ->
       log#ldebug
         (lazy
           ("end_abstraction_borrows: found borrow content: "
-          ^ borrow_content_to_string ~meta:(Some meta) ctx bc));
+          ^ borrow_content_to_string ~span:(Some span) ctx bc));
       let ctx =
         match bc with
         | VSharedBorrow bid -> (
             (* Replace the shared borrow with bottom *)
             let allow_inner_loans = false in
             match
-              end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx
+              end_borrow_get_borrow span (Some abs_id) allow_inner_loans bid ctx
             with
-            | Error _ -> craise __FILE__ __LINE__ meta "Unreachable"
+            | Error _ -> craise __FILE__ __LINE__ span "Unreachable"
             | Ok (ctx, _) ->
                 (* Give back *)
-                give_back_shared config meta bid ctx)
+                give_back_shared config span bid ctx)
         | VMutBorrow (bid, v) -> (
             (* Replace the mut borrow with bottom *)
             let allow_inner_loans = false in
             match
-              end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx
+              end_borrow_get_borrow span (Some abs_id) allow_inner_loans bid ctx
             with
-            | Error _ -> craise __FILE__ __LINE__ meta "Unreachable"
+            | Error _ -> craise __FILE__ __LINE__ span "Unreachable"
             | Ok (ctx, _) ->
                 (* Give the value back - note that the mut borrow was below a
                  * shared borrow: the value is thus unchanged *)
-                give_back_value config meta bid v ctx)
-        | VReservedMutBorrow _ -> craise __FILE__ __LINE__ meta "Unreachable"
+                give_back_value config span bid v ctx)
+        | VReservedMutBorrow _ -> craise __FILE__ __LINE__ span "Unreachable"
       in
       (* Reexplore *)
-      end_abstraction_borrows config meta chain abs_id ctx
+      end_abstraction_borrows config span chain abs_id ctx
 
 (** Remove an abstraction from the context, as well as all its references *)
-and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta)
+and end_abstraction_remove_from_context (_config : config) (span : Meta.span)
     (abs_id : AbstractionId.id) : cm_fun =
  fun ctx ->
-  let ctx, abs = ctx_remove_abs meta ctx abs_id in
+  let ctx, abs = ctx_remove_abs span ctx abs_id in
   let abs = Option.get abs in
   (* Synthesize the symbolic AST *)
   (ctx, SynthesizeSymbolic.synthesize_end_abstraction ctx abs)
@@ -1324,23 +1324,23 @@ and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta)
         intersecting proj_borrows, either in the concrete context or in an
         abstraction
 *)
-and end_proj_loans_symbolic (config : config) (meta : Meta.meta)
+and end_proj_loans_symbolic (config : config) (span : Meta.span)
     (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id)
     (regions : RegionId.Set.t) (sv : symbolic_value) : cm_fun =
  fun ctx ->
   (* Small helpers for sanity checks *)
-  let check ctx = no_aproj_over_symbolic_in_context meta sv ctx in
+  let check ctx = no_aproj_over_symbolic_in_context span sv ctx in
   (* Find the first proj_borrows which intersects the proj_loans *)
   let explore_shared = true in
   match
-    lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx
+    lookup_intersecting_aproj_borrows_opt span explore_shared regions sv ctx
   with
   | None ->
       (* We couldn't find any in the context: it means that the symbolic value
        * is in the concrete environment (or that we dropped it, in which case
        * it is completely absent). We thus simply need to replace the loans
        * projector with an ended projector. *)
-      let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in
+      let ctx = update_aproj_loans_to_ended span abs_id sv ctx in
       (* Sanity check *)
       check ctx;
       (* Continue *)
@@ -1383,16 +1383,16 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta)
             AbstractionId.Set.empty abs_ids
         in
         (* End the abstractions and continue *)
-        end_abstractions_aux config meta chain abs_ids ctx
+        end_abstractions_aux config span chain abs_ids ctx
       in
       (* End the internal borrows projectors and the loans projector *)
       let ctx =
         (* All the proj_borrows are owned: simply erase them *)
         let ctx =
-          remove_intersecting_aproj_borrows_shared meta regions sv ctx
+          remove_intersecting_aproj_borrows_shared span regions sv ctx
         in
         (* End the loan itself *)
-        update_aproj_loans_to_ended meta abs_id sv ctx
+        update_aproj_loans_to_ended span abs_id sv ctx
       in
       (* Sanity check *)
       check ctx;
@@ -1420,50 +1420,50 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta)
         *)
         (* End the projector of borrows - TODO: not completely sure what to
          * replace it with... Maybe we should introduce an ABottomProj? *)
-        let ctx = update_aproj_borrows meta abs_id sv AIgnoredProjBorrows ctx in
+        let ctx = update_aproj_borrows span abs_id sv AIgnoredProjBorrows ctx in
         (* Sanity check: no other occurrence of an intersecting projector of borrows *)
         sanity_check __FILE__ __LINE__
           (Option.is_none
-             (lookup_intersecting_aproj_borrows_opt meta explore_shared regions
+             (lookup_intersecting_aproj_borrows_opt span explore_shared regions
                 sv ctx))
-          meta;
+          span;
         (* End the projector of loans *)
-        let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in
+        let ctx = update_aproj_loans_to_ended span abs_id sv ctx in
         (* Sanity check *)
         check ctx;
         (* Continue *)
         (ctx, fun e -> e))
       else
         (* The borrows proj comes from a different abstraction: end it. *)
-        let ctx, cc = end_abstraction_aux config meta chain abs_id' ctx in
+        let ctx, cc = end_abstraction_aux config span chain abs_id' ctx in
         (* Retry ending the projector of loans *)
         let ctx, cc =
           comp cc
-            (end_proj_loans_symbolic config meta chain abs_id regions sv ctx)
+            (end_proj_loans_symbolic config span chain abs_id regions sv ctx)
         in
         (* Sanity check *)
         check ctx;
         (* Return *)
         (ctx, cc)
 
-let end_borrow config (meta : Meta.meta) : BorrowId.id -> cm_fun =
-  end_borrow_aux config meta [] None
+let end_borrow config (span : Meta.span) : BorrowId.id -> cm_fun =
+  end_borrow_aux config span [] None
 
-let end_borrows config (meta : Meta.meta) : BorrowId.Set.t -> cm_fun =
-  end_borrows_aux config meta [] None
+let end_borrows config (span : Meta.span) : BorrowId.Set.t -> cm_fun =
+  end_borrows_aux config span [] None
 
-let end_abstraction config meta = end_abstraction_aux config meta []
-let end_abstractions config meta = end_abstractions_aux config meta []
-let end_borrow_no_synth config meta id ctx = fst (end_borrow config meta id ctx)
+let end_abstraction config span = end_abstraction_aux config span []
+let end_abstractions config span = end_abstractions_aux config span []
+let end_borrow_no_synth config span id ctx = fst (end_borrow config span id ctx)
 
-let end_borrows_no_synth config meta ids ctx =
-  fst (end_borrows config meta ids ctx)
+let end_borrows_no_synth config span ids ctx =
+  fst (end_borrows config span ids ctx)
 
-let end_abstraction_no_synth config meta id ctx =
-  fst (end_abstraction config meta id ctx)
+let end_abstraction_no_synth config span id ctx =
+  fst (end_abstraction config span id ctx)
 
-let end_abstractions_no_synth config meta ids ctx =
-  fst (end_abstractions config meta ids ctx)
+let end_abstractions_no_synth config span ids ctx =
+  fst (end_abstractions config span ids ctx)
 
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
@@ -1481,14 +1481,14 @@ let end_abstractions_no_synth config meta ids ctx =
 
     The loan to update mustn't be a borrowed value.
  *)
-let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
+let promote_shared_loan_to_mut_loan (span : Meta.span) (l : BorrowId.id)
     (ctx : eval_ctx) : typed_value * eval_ctx =
   (* Debug *)
   log#ldebug
     (lazy
       ("promote_shared_loan_to_mut_loan:\n- loan: " ^ BorrowId.to_string l
      ^ "\n- context:\n"
-      ^ eval_ctx_to_string ~meta:(Some meta) ctx
+      ^ eval_ctx_to_string ~span:(Some span) ctx
       ^ "\n"));
   (* Lookup the shared loan - note that we can't promote a shared loan
    * in a shared value, but we can do it in a mutably borrowed value.
@@ -1497,34 +1497,34 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
   let ek =
     { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
   in
-  match lookup_loan meta ek l ctx with
+  match lookup_loan span ek l ctx with
   | _, Concrete (VMutLoan _) ->
-      craise __FILE__ __LINE__ meta "Expected a shared loan, found a mut loan"
+      craise __FILE__ __LINE__ span "Expected a shared loan, found a mut loan"
   | _, Concrete (VSharedLoan (bids, sv)) ->
       (* Check that there is only one borrow id (l) and update the loan *)
       cassert __FILE__ __LINE__
         (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1)
-        meta "There should only be one borrow id";
+        span "There should only be one borrow id";
       (* We need to check that there aren't any loans in the value:
          we should have gotten rid of those already, but it is better
          to do a sanity check. *)
-      sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) meta;
+      sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) span;
       (* Check there isn't {!Bottom} (this is actually an invariant *)
       cassert __FILE__ __LINE__
         (not (bottom_in_value ctx.ended_regions sv))
-        meta "There shouldn't be a bottom";
+        span "There shouldn't be a bottom";
       (* Check there aren't reserved borrows *)
       cassert __FILE__ __LINE__
         (not (reserved_in_value sv))
-        meta "There shouldn't be reserved borrows";
+        span "There shouldn't be reserved borrows";
       (* Update the loan content *)
-      let ctx = update_loan meta ek l (VMutLoan l) ctx in
+      let ctx = update_loan span ek l (VMutLoan l) ctx in
       (* Return *)
       (sv, ctx)
   | _, Abstract _ ->
       (* I don't think it is possible to have two-phase borrows involving borrows
          returned by abstractions. I'm not sure how we could handle that anyway. *)
-      craise __FILE__ __LINE__ meta
+      craise __FILE__ __LINE__ span
         "Can't promote a shared loan to a mutable loan if the loan is inside a \
          region abstraction"
 
@@ -1533,7 +1533,7 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
     This function updates a shared borrow to a mutable borrow (and that is
     all: it doesn't touch the corresponding loan).
  *)
-let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id)
+let replace_reserved_borrow_with_mut_borrow (span : Meta.span) (l : BorrowId.id)
     (borrowed_value : typed_value) (ctx : eval_ctx) : eval_ctx =
   (* Lookup the reserved borrow - note that we don't go inside borrows/loans:
      there can't be reserved borrows inside other borrows/loans
@@ -1541,28 +1541,28 @@ let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id)
   let ek =
     { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false }
   in
-  match lookup_borrow meta ek l ctx with
+  match lookup_borrow span ek l ctx with
   | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) ->
-      craise __FILE__ __LINE__ meta "Expected a reserved mutable borrow"
+      craise __FILE__ __LINE__ span "Expected a reserved mutable borrow"
   | Concrete (VReservedMutBorrow _) ->
       (* Update it *)
-      update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx
+      update_borrow span ek l (VMutBorrow (l, borrowed_value)) ctx
   | Abstract _ ->
       (* This can't happen for sure *)
-      craise __FILE__ __LINE__ meta
+      craise __FILE__ __LINE__ span
         "Can't promote a shared borrow to a mutable borrow if the borrow is \
          inside a region abstraction"
 
 (** Promote a reserved mut borrow to a mut borrow. *)
-let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta)
+let rec promote_reserved_mut_borrow (config : config) (span : Meta.span)
     (l : BorrowId.id) : cm_fun =
  fun ctx ->
   (* Lookup the value *)
   let ek =
     { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
   in
-  match lookup_loan meta ek l ctx with
-  | _, Concrete (VMutLoan _) -> craise __FILE__ __LINE__ meta "Unreachable"
+  match lookup_loan span ek l ctx with
+  | _, Concrete (VMutLoan _) -> craise __FILE__ __LINE__ span "Unreachable"
   | _, Concrete (VSharedLoan (bids, sv)) -> (
       (* If there are loans inside the value, end them. Note that there can't be
          reserved borrows inside the value.
@@ -1572,46 +1572,46 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta)
           (* End the loans *)
           let ctx, cc =
             match lc with
-            | VSharedLoan (bids, _) -> end_borrows config meta bids ctx
-            | VMutLoan bid -> end_borrow config meta bid ctx
+            | VSharedLoan (bids, _) -> end_borrows config span bids ctx
+            | VMutLoan bid -> end_borrow config span bid ctx
           in
           (* Recursive call *)
-          comp cc (promote_reserved_mut_borrow config meta l ctx)
+          comp cc (promote_reserved_mut_borrow config span l ctx)
       | None ->
           (* No loan to end inside the value *)
           (* Some sanity checks *)
           log#ldebug
             (lazy
               ("activate_reserved_mut_borrow: resulting value:\n"
-              ^ typed_value_to_string ~meta:(Some meta) ctx sv));
-          sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) meta;
+              ^ typed_value_to_string ~span:(Some span) ctx sv));
+          sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) span;
           sanity_check __FILE__ __LINE__
             (not (bottom_in_value ctx.ended_regions sv))
-            meta;
-          sanity_check __FILE__ __LINE__ (not (reserved_in_value sv)) meta;
+            span;
+          sanity_check __FILE__ __LINE__ (not (reserved_in_value sv)) span;
           (* End the borrows which borrow from the value, at the exception of
              the borrow we want to promote *)
           let bids = BorrowId.Set.remove l bids in
-          let ctx, cc = end_borrows config meta bids ctx in
+          let ctx, cc = end_borrows config span bids ctx in
           (* Promote the loan - TODO: this will fail if the value contains
            * any loans. In practice, it shouldn't, but we could also
            * look for loans inside the value and end them before promoting
            * the borrow. *)
-          let v, ctx = promote_shared_loan_to_mut_loan meta l ctx in
+          let v, ctx = promote_shared_loan_to_mut_loan span l ctx in
           (* Promote the borrow - the value should have been checked by
              {!promote_shared_loan_to_mut_loan}
           *)
-          let ctx = replace_reserved_borrow_with_mut_borrow meta l v ctx in
+          let ctx = replace_reserved_borrow_with_mut_borrow span l v ctx in
           (* Return *)
           (ctx, cc))
   | _, Abstract _ ->
       (* I don't think it is possible to have two-phase borrows involving borrows
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
-      craise __FILE__ __LINE__ meta
+      craise __FILE__ __LINE__ span
         "Can't activate a reserved mutable borrow referencing a loan inside\n\
         \         a region abstraction"
 
-let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
+let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
     (destructure_shared_values : bool) (ctx : eval_ctx) (abs0 : abs) : abs =
   (* Accumulator to store the destructured values *)
   let avalues = ref [] in
@@ -1624,7 +1624,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
      ignore the children altogether. Instead, we explore them and make sure
      we don't register values while doing so.
   *)
-  let push_fail _ = craise __FILE__ __LINE__ meta "Unreachable" in
+  let push_fail _ = craise __FILE__ __LINE__ span "Unreachable" in
   (* Function to explore an avalue and destructure it *)
   let rec list_avalues (allow_borrows : bool) (push : typed_avalue -> unit)
       (av : typed_avalue) : unit =
@@ -1641,13 +1641,13 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             (* We don't support nested borrows for now *)
             cassert __FILE__ __LINE__
               (not (value_has_borrows ctx sv.value))
-              meta "Nested borrows are not supported yet";
+              span "Nested borrows are not supported yet";
             (* Destructure the shared value *)
             let avl, sv =
               if destructure_shared_values then list_values sv else ([], sv)
             in
             (* Push a value *)
-            let ignored = mk_aignored meta child_av.ty in
+            let ignored = mk_aignored span child_av.ty in
             let value = ALoan (ASharedLoan (bids, sv, ignored)) in
             push { value; ty };
             (* Explore the child *)
@@ -1663,39 +1663,39 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             (* Explore the child *)
             list_avalues false push_fail child_av;
             (* Explore the whole loan *)
-            let ignored = mk_aignored meta child_av.ty in
+            let ignored = mk_aignored span child_av.ty in
             let value = ALoan (AMutLoan (bid, ignored)) in
             push { value; ty }
         | AIgnoredMutLoan (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
             cassert __FILE__ __LINE__
               (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
-              meta "Nested borrows are not supported yet";
-            sanity_check __FILE__ __LINE__ (opt_bid = None) meta;
+              span "Nested borrows are not supported yet";
+            sanity_check __FILE__ __LINE__ (opt_bid = None) span;
             (* Simply explore the child *)
             list_avalues false push_fail child_av
         | AEndedMutLoan
-            { child = child_av; given_back = _; given_back_meta = _ }
+            { child = child_av; given_back = _; given_back_span = _ }
         | AEndedSharedLoan (_, child_av)
         | AEndedIgnoredMutLoan
-            { child = child_av; given_back = _; given_back_meta = _ }
+            { child = child_av; given_back = _; given_back_span = _ }
         | AIgnoredSharedLoan child_av ->
             (* We don't support nested borrows for now *)
             cassert __FILE__ __LINE__
               (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
-              meta "Nested borrows are not supported yet";
+              span "Nested borrows are not supported yet";
             (* Simply explore the child *)
             list_avalues false push_fail child_av)
     | ABorrow bc -> (
         (* Sanity check - rem.: may be redundant with [push_fail] *)
-        sanity_check __FILE__ __LINE__ allow_borrows meta;
+        sanity_check __FILE__ __LINE__ allow_borrows span;
         (* Explore the borrow content *)
         match bc with
         | AMutBorrow (bid, child_av) ->
             (* Explore the child *)
             list_avalues false push_fail child_av;
             (* Explore the borrow *)
-            let ignored = mk_aignored meta child_av.ty in
+            let ignored = mk_aignored span child_av.ty in
             let value = ABorrow (AMutBorrow (bid, ignored)) in
             push { value; ty }
         | ASharedBorrow _ ->
@@ -1705,21 +1705,21 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             (* We don't support nested borrows for now *)
             cassert __FILE__ __LINE__
               (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
-              meta "Nested borrows are not supported yet";
-            sanity_check __FILE__ __LINE__ (opt_bid = None) meta;
+              span "Nested borrows are not supported yet";
+            sanity_check __FILE__ __LINE__ (opt_bid = None) span;
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | AEndedIgnoredMutBorrow
-            { child = child_av; given_back = _; given_back_meta = _ } ->
+            { child = child_av; given_back = _; given_back_span = _ } ->
             (* We don't support nested borrows for now *)
             cassert __FILE__ __LINE__
               (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
-              meta "Nested borrows are not supported yet";
+              span "Nested borrows are not supported yet";
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | AProjSharedBorrow asb ->
             (* We don't support nested borrows *)
-            cassert __FILE__ __LINE__ (asb = []) meta
+            cassert __FILE__ __LINE__ (asb = []) span
               "Nested borrows are not supported yet";
             (* Nothing specific to do *)
             ()
@@ -1728,13 +1728,13 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
                be in the context anymore (if we end *one* borrow in an abstraction,
                we have to end them all and remove the abstraction from the context)
             *)
-            craise __FILE__ __LINE__ meta "Unreachable")
+            craise __FILE__ __LINE__ span "Unreachable")
     | ASymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
         sanity_check __FILE__ __LINE__
           (not (ty_has_borrows ctx.type_ctx.type_infos ty))
-          meta
+          span
   and list_values (v : typed_value) : typed_avalue list * typed_value =
     let ty = v.ty in
     match v.value with
@@ -1746,22 +1746,22 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
         let avl = List.concat avll in
         let adt = { adt with field_values } in
         (avl, { v with value = VAdt adt })
-    | VBottom -> craise __FILE__ __LINE__ meta "Unreachable"
+    | VBottom -> craise __FILE__ __LINE__ span "Unreachable"
     | VBorrow _ ->
         (* We don't support nested borrows for now *)
-        craise __FILE__ __LINE__ meta "Unreachable"
+        craise __FILE__ __LINE__ span "Unreachable"
     | VLoan lc -> (
         match lc with
         | VSharedLoan (bids, sv) ->
             let avl, sv = list_values sv in
             if destructure_shared_values then (
               (* Rem.: the shared value can't contain loans nor borrows *)
-              cassert __FILE__ __LINE__ (ty_no_regions ty) meta
+              cassert __FILE__ __LINE__ (ty_no_regions ty) span
                 "Nested borrows are not supported yet";
               let av : typed_avalue =
                 sanity_check __FILE__ __LINE__
                   (not (value_has_loans_or_borrows ctx sv.value))
-                  meta;
+                  span;
                 (* We introduce fresh ids for the symbolic values *)
                 let mk_value_with_fresh_sids (v : typed_value) : typed_value =
                   let visitor =
@@ -1777,20 +1777,20 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
                 let sv = mk_value_with_fresh_sids sv in
                 (* Create the new avalue *)
                 let value =
-                  ALoan (ASharedLoan (bids, sv, mk_aignored meta ty))
+                  ALoan (ASharedLoan (bids, sv, mk_aignored span ty))
                 in
                 { value; ty }
               in
               let avl = List.append [ av ] avl in
               (avl, sv))
             else (avl, { v with value = VLoan (VSharedLoan (bids, sv)) })
-        | VMutLoan _ -> craise __FILE__ __LINE__ meta "Unreachable")
+        | VMutLoan _ -> craise __FILE__ __LINE__ span "Unreachable")
     | VSymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
         sanity_check __FILE__ __LINE__
           (not (ty_has_borrows ctx.type_ctx.type_infos ty))
-          meta;
+          span;
         ([], v)
   in
 
@@ -1800,14 +1800,14 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
   (* Update *)
   { abs0 with avalues; kind = abs_kind; can_end }
 
-let abs_is_destructured (meta : Meta.meta) (destructure_shared_values : bool)
+let abs_is_destructured (span : Meta.span) (destructure_shared_values : bool)
     (ctx : eval_ctx) (abs : abs) : bool =
   let abs' =
-    destructure_abs meta abs.kind abs.can_end destructure_shared_values ctx abs
+    destructure_abs span abs.kind abs.can_end destructure_shared_values ctx abs
   in
   abs = abs'
 
-let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
+let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
     (can_end : bool) (destructure_shared_values : bool) (ctx : eval_ctx)
     (v : typed_value) : abs list =
   (* Convert the value to a list of avalues *)
@@ -1846,7 +1846,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
     log#ldebug
       (lazy
         ("convert_value_to_abstractions: to_avalues:\n- value: "
-        ^ typed_value_to_string ~meta:(Some meta) ctx v));
+        ^ typed_value_to_string ~span:(Some span) ctx v));
 
     let ty = v.ty in
     match v.value with
@@ -1890,14 +1890,14 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
         (avl, { v with value = VAdt adt })
     | VBorrow bc -> (
         let _, ref_ty, kind = ty_as_ref ty in
-        cassert __FILE__ __LINE__ (ty_no_regions ref_ty) meta
+        cassert __FILE__ __LINE__ (ty_no_regions ref_ty) span
           "Nested borrows are not supported yet";
         (* Sanity check *)
-        sanity_check __FILE__ __LINE__ allow_borrows meta;
+        sanity_check __FILE__ __LINE__ allow_borrows span;
         (* Convert the borrow content *)
         match bc with
         | VSharedBorrow bid ->
-            cassert __FILE__ __LINE__ (ty_no_regions ref_ty) meta
+            cassert __FILE__ __LINE__ (ty_no_regions ref_ty) span
               "Nested borrows are not supported yet";
             let ty = TRef (RFVar r_id, ref_ty, kind) in
             let value = ABorrow (ASharedBorrow bid) in
@@ -1907,10 +1907,10 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
             (* We don't support nested borrows for now *)
             cassert __FILE__ __LINE__
               (not (value_has_borrows ctx bv.value))
-              meta "Nested borrows are not supported yet";
+              span "Nested borrows are not supported yet";
             (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
             let ty = TRef (RFVar r_id, ref_ty, kind) in
-            let ignored = mk_aignored meta ref_ty in
+            let ignored = mk_aignored span ref_ty in
             let av = ABorrow (AMutBorrow (bid, ignored)) in
             let av = { value = av; ty } in
             (* Continue exploring, looking for loans (and forbidding borrows,
@@ -1920,7 +1920,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
             (av :: avl, value)
         | VReservedMutBorrow _ ->
             (* This borrow should have been activated *)
-            craise __FILE__ __LINE__ meta "Unexpected")
+            craise __FILE__ __LINE__ span "Unexpected")
     | VLoan lc -> (
         match lc with
         | VSharedLoan (bids, sv) ->
@@ -1928,13 +1928,13 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
             (* We don't support nested borrows for now *)
             cassert __FILE__ __LINE__
               (not (value_has_borrows ctx sv.value))
-              meta "Nested borrows are not supported yet";
+              span "Nested borrows are not supported yet";
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
-            cassert __FILE__ __LINE__ (ty_no_regions ty) meta
+            cassert __FILE__ __LINE__ (ty_no_regions ty) span
               "Nested borrows are not supported yet";
             let ty = mk_ref_ty (RFVar r_id) ty RShared in
-            let ignored = mk_aignored meta ty in
+            let ignored = mk_aignored span ty in
             (* Rem.: the shared value might contain loans *)
             let avl, sv = to_avalues false true true r_id sv in
             let av = ALoan (ASharedLoan (bids, sv, ignored)) in
@@ -1950,10 +1950,10 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
         | VMutLoan bid ->
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
-            cassert __FILE__ __LINE__ (ty_no_regions ty) meta
+            cassert __FILE__ __LINE__ (ty_no_regions ty) span
               "Nested borrows are not supported yet";
             let ty = mk_ref_ty (RFVar r_id) ty RMut in
-            let ignored = mk_aignored meta ty in
+            let ignored = mk_aignored span ty in
             let av = ALoan (AMutLoan (bid, ignored)) in
             let av = { value = av; ty } in
             ([ av ], v))
@@ -1962,7 +1962,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
            be eagerly expanded, and we don't support nested borrows *)
         cassert __FILE__ __LINE__
           (not (value_has_borrows ctx v.value))
-          meta "Nested borrows are not supported yet";
+          span "Nested borrows are not supported yet";
         (* Return nothing *)
         ([], v)
   in
@@ -2003,7 +2003,7 @@ type merge_abstraction_info = {
     - all the borrows are destructured (for instance, shared loans can't
       contain shared loans).
  *)
-let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
+let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
     (abs : abs) : merge_abstraction_info =
   let loans : loan_id_set ref = ref BorrowId.Set.empty in
   let borrows : borrow_id_set ref = ref BorrowId.Set.empty in
@@ -2016,32 +2016,32 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
   in
 
   let push_loans ids (lc : g_loan_content_with_ty) : unit =
-    sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint !loans ids) meta;
+    sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint !loans ids) span;
     loans := BorrowId.Set.union !loans ids;
     BorrowId.Set.iter
       (fun id ->
         sanity_check __FILE__ __LINE__
           (not (BorrowId.Map.mem id !loan_to_content))
-          meta;
+          span;
         loan_to_content := BorrowId.Map.add id lc !loan_to_content;
         borrows_loans := LoanId id :: !borrows_loans)
       ids
   in
   let push_loan id (lc : g_loan_content_with_ty) : unit =
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !loans)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !loans)) span;
     loans := BorrowId.Set.add id !loans;
     sanity_check __FILE__ __LINE__
       (not (BorrowId.Map.mem id !loan_to_content))
-      meta;
+      span;
     loan_to_content := BorrowId.Map.add id lc !loan_to_content;
     borrows_loans := LoanId id :: !borrows_loans
   in
   let push_borrow id (bc : g_borrow_content_with_ty) : unit =
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !borrows)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !borrows)) span;
     borrows := BorrowId.Set.add id !borrows;
     sanity_check __FILE__ __LINE__
       (not (BorrowId.Map.mem id !borrow_to_content))
-      meta;
+      span;
     borrow_to_content := BorrowId.Map.add id bc !borrow_to_content;
     borrows_loans := BorrowId id :: !borrows_loans
   in
@@ -2064,23 +2064,23 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
         let ty =
           match Option.get env with
           | Concrete ty -> ty
-          | Abstract _ -> craise __FILE__ __LINE__ meta "Unreachable"
+          | Abstract _ -> craise __FILE__ __LINE__ span "Unreachable"
         in
         (match lc with
         | VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc))
-        | VMutLoan _ -> craise __FILE__ __LINE__ meta "Unreachable");
+        | VMutLoan _ -> craise __FILE__ __LINE__ span "Unreachable");
         (* Continue *)
         super#visit_loan_content env lc
 
       method! visit_borrow_content _ _ =
         (* Can happen if we explore shared values which contain borrows -
            i.e., if we have nested borrows (we forbid this for now) *)
-        craise __FILE__ __LINE__ meta "Unreachable"
+        craise __FILE__ __LINE__ span "Unreachable"
 
       method! visit_aloan_content env lc =
         let ty =
           match Option.get env with
-          | Concrete _ -> craise __FILE__ __LINE__ meta "Unreachable"
+          | Concrete _ -> craise __FILE__ __LINE__ span "Unreachable"
           | Abstract ty -> ty
         in
         (* Register the loans *)
@@ -2090,14 +2090,14 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
         | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _
         | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ ->
             (* The abstraction has been destructured, so those shouldn't appear *)
-            craise __FILE__ __LINE__ meta "Unreachable");
+            craise __FILE__ __LINE__ span "Unreachable");
         (* Continue *)
         super#visit_aloan_content env lc
 
       method! visit_aborrow_content env bc =
         let ty =
           match Option.get env with
-          | Concrete _ -> craise __FILE__ __LINE__ meta "Unreachable"
+          | Concrete _ -> craise __FILE__ __LINE__ span "Unreachable"
           | Abstract ty -> ty
         in
         (* Explore the borrow content *)
@@ -2111,20 +2111,20 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
               | AsbProjReborrows _ ->
                   (* Can only happen if the symbolic value (potentially) contains
                      borrows - i.e., we have nested borrows *)
-                  craise __FILE__ __LINE__ meta "Unreachable"
+                  craise __FILE__ __LINE__ span "Unreachable"
             in
             List.iter register asb
         | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedMutBorrow _
         | AEndedSharedBorrow ->
             (* The abstraction has been destructured, so those shouldn't appear *)
-            craise __FILE__ __LINE__ meta "Unreachable");
+            craise __FILE__ __LINE__ span "Unreachable");
         super#visit_aborrow_content env bc
 
       method! visit_symbolic_value _ sv =
         (* Sanity check: no borrows *)
         sanity_check __FILE__ __LINE__
           (not (symbolic_value_has_borrows ctx sv))
-          meta
+          span
     end
   in
 
@@ -2191,25 +2191,25 @@ type merge_duplicates_funcs = {
 
     Merge two abstractions into one, without updating the context.
  *)
-let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
+let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
     (can_end : bool) (merge_funs : merge_duplicates_funcs option)
     (ctx : eval_ctx) (abs0 : abs) (abs1 : abs) : abs =
   log#ldebug
     (lazy
       ("merge_into_abstraction_aux:\n- abs0:\n"
-      ^ abs_to_string meta ctx abs0
+      ^ abs_to_string span ctx abs0
       ^ "\n\n- abs1:\n"
-      ^ abs_to_string meta ctx abs1));
+      ^ abs_to_string span ctx abs1));
 
   (* Check that the abstractions are destructured *)
   if !Config.sanity_checks then (
     let destructure_shared_values = true in
     sanity_check __FILE__ __LINE__
-      (abs_is_destructured meta destructure_shared_values ctx abs0)
-      meta;
+      (abs_is_destructured span destructure_shared_values ctx abs0)
+      span;
     sanity_check __FILE__ __LINE__
-      (abs_is_destructured meta destructure_shared_values ctx abs1)
-      meta);
+      (abs_is_destructured span destructure_shared_values ctx abs1)
+      span);
 
   (* Compute the relevant information *)
   let {
@@ -2219,7 +2219,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
     loan_to_content = loan_to_content0;
     borrow_to_content = borrow_to_content0;
   } =
-    compute_merge_abstraction_info meta ctx abs0
+    compute_merge_abstraction_info span ctx abs0
   in
 
   let {
@@ -2229,7 +2229,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
     loan_to_content = loan_to_content1;
     borrow_to_content = borrow_to_content1;
   } =
-    compute_merge_abstraction_info meta ctx abs1
+    compute_merge_abstraction_info span ctx abs1
   in
 
   (* Sanity check: there is no loan/borrows which appears in both abstractions,
@@ -2237,8 +2237,8 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
   if merge_funs = None then (
     sanity_check __FILE__ __LINE__
       (BorrowId.Set.disjoint borrows0 borrows1)
-      meta;
-    sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) meta);
+      span;
+    sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) span);
 
   (* Merge.
      There are several cases:
@@ -2265,7 +2265,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
     log#ldebug
       (lazy
         ("merge_into_abstraction_aux: push_avalue: "
-        ^ typed_avalue_to_string ~meta:(Some meta) ctx av));
+        ^ typed_avalue_to_string ~span:(Some span) ctx av));
     avalues := av :: !avalues
   in
   let push_opt_avalue av =
@@ -2279,7 +2279,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
   in
   let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t =
     let bids = BorrowId.Set.diff bids intersect in
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) span;
     bids
   in
   let filter_bid (bid : BorrowId.id) : BorrowId.id option =
@@ -2307,11 +2307,11 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
         (Option.get merge_funs).merge_ashared_borrows id ty0 ty1
     | AProjSharedBorrow _, AProjSharedBorrow _ ->
         (* Unreachable because requires nested borrows *)
-        craise __FILE__ __LINE__ meta "Unreachable"
+        craise __FILE__ __LINE__ span "Unreachable"
     | _ ->
         (* Unreachable because those cases are ignored (ended/ignored borrows)
            or inconsistent *)
-        craise __FILE__ __LINE__ meta "Unreachable"
+        craise __FILE__ __LINE__ span "Unreachable"
   in
 
   let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty)
@@ -2319,12 +2319,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
     match (bc0, bc1) with
     | Concrete _, Concrete _ ->
         (* This can happen only in case of nested borrows *)
-        craise __FILE__ __LINE__ meta "Unreachable"
+        craise __FILE__ __LINE__ span "Unreachable"
     | Abstract (ty0, bc0), Abstract (ty1, bc1) ->
         merge_aborrow_contents ty0 bc0 ty1 bc1
     | Concrete _, Abstract _ | Abstract _, Concrete _ ->
         (* TODO: is it really unreachable? *)
-        craise __FILE__ __LINE__ meta "Unreachable"
+        craise __FILE__ __LINE__ span "Unreachable"
   in
 
   let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty)
@@ -2342,7 +2342,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
         (* Check that the sets of ids are the same - if it is not the case, it
            means we actually need to merge more than 2 avalues: we ignore this
            case for now *)
-        sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) meta;
+        sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) span;
         let ids = ids0 in
         if BorrowId.Set.is_empty ids then (
           (* If the set of ids is empty, we can eliminate this shared loan.
@@ -2356,12 +2356,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
           *)
           sanity_check __FILE__ __LINE__
             (not (value_has_loans_or_borrows ctx sv0.value))
-            meta;
+            span;
           sanity_check __FILE__ __LINE__
             (not (value_has_loans_or_borrows ctx sv0.value))
-            meta;
-          sanity_check __FILE__ __LINE__ (is_aignored child0.value) meta;
-          sanity_check __FILE__ __LINE__ (is_aignored child1.value) meta;
+            span;
+          sanity_check __FILE__ __LINE__ (is_aignored child0.value) span;
+          sanity_check __FILE__ __LINE__ (is_aignored child1.value) span;
           None)
         else (
           (* Register the loan ids *)
@@ -2373,7 +2373,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
     | _ ->
         (* Unreachable because those cases are ignored (ended/ignored borrows)
            or inconsistent *)
-        craise __FILE__ __LINE__ meta "Unreachable"
+        craise __FILE__ __LINE__ span "Unreachable"
   in
 
   (* Note that because we may filter ids from a set of id, this function has
@@ -2384,12 +2384,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
     match (lc0, lc1) with
     | Concrete _, Concrete _ ->
         (* This can not happen: the values should have been destructured *)
-        craise __FILE__ __LINE__ meta "Unreachable"
+        craise __FILE__ __LINE__ span "Unreachable"
     | Abstract (ty0, lc0), Abstract (ty1, lc1) ->
         merge_aloan_contents ty0 lc0 ty1 lc1
     | Concrete _, Abstract _ | Abstract _, Concrete _ ->
         (* TODO: is it really unreachable? *)
-        craise __FILE__ __LINE__ meta "Unreachable"
+        craise __FILE__ __LINE__ span "Unreachable"
   in
 
   (* Note that we first explore the borrows/loans of [abs1], because we
@@ -2430,12 +2430,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
                              a concrete borrow can only happen inside a shared
                              loan
                           *)
-                          craise __FILE__ __LINE__ meta "Unreachable"
+                          craise __FILE__ __LINE__ span "Unreachable"
                       | Abstract (ty, bc) -> { value = ABorrow bc; ty })
                   | Some bc0, Some bc1 ->
-                      sanity_check __FILE__ __LINE__ (merge_funs <> None) meta;
+                      sanity_check __FILE__ __LINE__ (merge_funs <> None) span;
                       merge_g_borrow_contents bc0 bc1
-                  | None, None -> craise __FILE__ __LINE__ meta "Unreachable"
+                  | None, None -> craise __FILE__ __LINE__ span "Unreachable"
                 in
                 push_avalue av)
       | LoanId bid ->
@@ -2468,19 +2468,19 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
                       | Concrete _ ->
                           (* This shouldn't happen because the avalues should
                              have been destructured. *)
-                          craise __FILE__ __LINE__ meta "Unreachable"
+                          craise __FILE__ __LINE__ span "Unreachable"
                       | Abstract (ty, lc) -> (
                           match lc with
                           | ASharedLoan (bids, sv, child) ->
                               let bids = filter_bids bids in
                               sanity_check __FILE__ __LINE__
                                 (not (BorrowId.Set.is_empty bids))
-                                meta;
+                                span;
                               sanity_check __FILE__ __LINE__
-                                (is_aignored child.value) meta;
+                                (is_aignored child.value) span;
                               sanity_check __FILE__ __LINE__
                                 (not (value_has_loans_or_borrows ctx sv.value))
-                                meta;
+                                span;
                               let lc = ASharedLoan (bids, sv, child) in
                               set_loans_as_merged bids;
                               Some { value = ALoan lc; ty }
@@ -2491,11 +2491,11 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
                           | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _
                           | AIgnoredSharedLoan _ ->
                               (* The abstraction has been destructured, so those shouldn't appear *)
-                              craise __FILE__ __LINE__ meta "Unreachable"))
+                              craise __FILE__ __LINE__ span "Unreachable"))
                   | Some lc0, Some lc1 ->
-                      sanity_check __FILE__ __LINE__ (merge_funs <> None) meta;
+                      sanity_check __FILE__ __LINE__ (merge_funs <> None) span;
                       merge_g_loan_contents lc0 lc1
-                  | None, None -> craise __FILE__ __LINE__ meta "Unreachable"
+                  | None, None -> craise __FILE__ __LINE__ span "Unreachable"
                 in
                 push_opt_avalue av))
     borrows_loans;
@@ -2513,7 +2513,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
       match av.value with
       | ABorrow _ -> true
       | ALoan _ -> false
-      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ span "Unexpected"
     in
     let aborrows, aloans = List.partition is_borrow avalues in
     List.append aborrows aloans
@@ -2548,7 +2548,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
   in
 
   (* Sanity check *)
-  sanity_check __FILE__ __LINE__ (abs_is_destructured meta true ctx abs) meta;
+  sanity_check __FILE__ __LINE__ (abs_is_destructured span true ctx abs) span;
   (* Return *)
   abs
 
@@ -2559,7 +2559,7 @@ let ctx_merge_regions (ctx : eval_ctx) (rid : RegionId.id)
   let env = Substitute.env_subst_rids rsubst ctx.env in
   { ctx with env }
 
-let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind)
+let merge_into_abstraction (span : Meta.span) (abs_kind : abs_kind)
     (can_end : bool) (merge_funs : merge_duplicates_funcs option)
     (ctx : eval_ctx) (abs_id0 : AbstractionId.id) (abs_id1 : AbstractionId.id) :
     eval_ctx * AbstractionId.id =
@@ -2569,13 +2569,13 @@ let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind)
 
   (* Merge them *)
   let nabs =
-    merge_into_abstraction_aux meta abs_kind can_end merge_funs ctx abs0 abs1
+    merge_into_abstraction_aux span abs_kind can_end merge_funs ctx abs0 abs1
   in
 
   (* Update the environment: replace the abstraction 1 with the result of the merge,
      remove the abstraction 0 *)
-  let ctx = fst (ctx_subst_abs meta ctx abs_id1 nabs) in
-  let ctx = fst (ctx_remove_abs meta ctx abs_id0) in
+  let ctx = fst (ctx_subst_abs span ctx abs_id1 nabs) in
+  let ctx = fst (ctx_remove_abs span ctx abs_id0) in
 
   (* Merge all the regions from the abstraction into one (the first - i.e., the
      one with the smallest id). Note that we need to do this in the whole
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 30b75790..56df9344 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -9,39 +9,39 @@ open Cps
     the set of borrows tracked by a shared value, referenced by the
     [original_bid] argument.  *)
 val reborrow_shared :
-  Meta.meta -> BorrowId.id -> BorrowId.id -> eval_ctx -> eval_ctx
+  Meta.span -> BorrowId.id -> BorrowId.id -> eval_ctx -> eval_ctx
 
 (** End a borrow identified by its id, while preserving the invariants.
 
     If the borrow is inside another borrow/an abstraction or contains loans,
     [end_borrow] will end those borrows/abstractions/loans first.
   *)
-val end_borrow : config -> Meta.meta -> BorrowId.id -> cm_fun
+val end_borrow : config -> Meta.span -> BorrowId.id -> cm_fun
 
 (** End a set of borrows identified by their ids, while preserving the invariants. *)
-val end_borrows : config -> Meta.meta -> BorrowId.Set.t -> cm_fun
+val end_borrows : config -> Meta.span -> BorrowId.Set.t -> cm_fun
 
 (** End an abstraction while preserving the invariants. *)
-val end_abstraction : config -> Meta.meta -> AbstractionId.id -> cm_fun
+val end_abstraction : config -> Meta.span -> AbstractionId.id -> cm_fun
 
 (** End a set of abstractions while preserving the invariants. *)
-val end_abstractions : config -> Meta.meta -> AbstractionId.Set.t -> cm_fun
+val end_abstractions : config -> Meta.span -> AbstractionId.Set.t -> cm_fun
 
 (** End a borrow and return the resulting environment, ignoring synthesis *)
 val end_borrow_no_synth :
-  config -> Meta.meta -> BorrowId.id -> eval_ctx -> eval_ctx
+  config -> Meta.span -> BorrowId.id -> eval_ctx -> eval_ctx
 
 (** End a set of borrows and return the resulting environment, ignoring synthesis *)
 val end_borrows_no_synth :
-  config -> Meta.meta -> BorrowId.Set.t -> eval_ctx -> eval_ctx
+  config -> Meta.span -> BorrowId.Set.t -> eval_ctx -> eval_ctx
 
 (** End an abstraction and return the resulting environment, ignoring synthesis *)
 val end_abstraction_no_synth :
-  config -> Meta.meta -> AbstractionId.id -> eval_ctx -> eval_ctx
+  config -> Meta.span -> AbstractionId.id -> eval_ctx -> eval_ctx
 
 (** End a set of abstractions and return the resulting environment, ignoring synthesis *)
 val end_abstractions_no_synth :
-  config -> Meta.meta -> AbstractionId.Set.t -> eval_ctx -> eval_ctx
+  config -> Meta.span -> AbstractionId.Set.t -> eval_ctx -> eval_ctx
 
 (** Promote a reserved mut borrow to a mut borrow, while preserving the invariants.
 
@@ -52,7 +52,7 @@ val end_abstractions_no_synth :
     the corresponding shared loan with a mutable loan (after having ended the
     other shared borrows which point to this loan).
  *)
-val promote_reserved_mut_borrow : config -> Meta.meta -> BorrowId.id -> cm_fun
+val promote_reserved_mut_borrow : config -> Meta.span -> BorrowId.id -> cm_fun
 
 (** Transform an abstraction to an abstraction where the values are not
     structured.
@@ -95,7 +95,7 @@ val promote_reserved_mut_borrow : config -> Meta.meta -> BorrowId.id -> cm_fun
     - [abs]
  *)
 val destructure_abs :
-  Meta.meta -> abs_kind -> bool -> bool -> eval_ctx -> abs -> abs
+  Meta.span -> abs_kind -> bool -> bool -> eval_ctx -> abs -> abs
 
 (** Return [true] if the values in an abstraction are destructured.
 
@@ -103,7 +103,7 @@ val destructure_abs :
 
     The input boolean is [destructure_shared_value]. See {!destructure_abs}.
  *)
-val abs_is_destructured : Meta.meta -> bool -> eval_ctx -> abs -> bool
+val abs_is_destructured : Meta.span -> bool -> eval_ctx -> abs -> bool
 
 (** Turn a value into a abstractions.
 
@@ -129,7 +129,7 @@ val abs_is_destructured : Meta.meta -> bool -> eval_ctx -> abs -> bool
     - [v]
  *)
 val convert_value_to_abstractions :
-  Meta.meta -> abs_kind -> bool -> bool -> eval_ctx -> typed_value -> abs list
+  Meta.span -> abs_kind -> bool -> bool -> eval_ctx -> typed_value -> abs list
 
 (** See {!merge_into_abstraction}.
 
@@ -236,7 +236,7 @@ type merge_duplicates_funcs = {
     results from the merge.
  *)
 val merge_into_abstraction :
-  Meta.meta ->
+  Meta.span ->
   abs_kind ->
   bool ->
   merge_duplicates_funcs option ->