From 9d27e2e27db06eaad7565b55366ca8734b364fca Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 2 Aug 2023 11:03:59 +0200
Subject: Make progress proapagating the changes

---
 compiler/InterpreterProjectors.mli | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'compiler/InterpreterProjectors.mli')

diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
index 1afb9d53..bcc3dee2 100644
--- a/compiler/InterpreterProjectors.mli
+++ b/compiler/InterpreterProjectors.mli
@@ -55,7 +55,16 @@ val prepare_reborrows :
   bool ->
   (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx)
 
-(** Apply (and reduce) a projector over borrows to a value.
+(** Apply (and reduce) a projector over borrows to an avalue.
+    We use this for instance to spread the borrows present in the inputs
+    of a function into the regions introduced for this function. For instance:
+    {[
+      fn f<'a, 'b, T>(x: &'a T, y: &'b T)
+    ]}
+    If we call `f` with `x -> shared_borrow l0` and `y -> shared_borrow l1`, then
+    for the region introduced for `'a` we need to project the value for `x` to
+    a shared aborrow, and we need to ignore the borrow in `y`, because it belongs
+    to the other region.
 
     Parameters:
     - [check_symbolic_no_ended]: controls whether we check or not whether
-- 
cgit v1.2.3