From 592a2113734078290d4406df7804bfc128865958 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jan 2022 23:11:05 +0100
Subject: Use msymbolic_value instead of mvalue in some places in Values.aproj

---
 src/Values.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'src/Values.ml')

diff --git a/src/Values.ml b/src/Values.ml
index fe8daf30..6ab81f6b 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -252,7 +252,7 @@ class ['self] map_aproj_base =
   end
 
 type aproj =
-  | AProjLoans of symbolic_value * (mvalue * aproj) list
+  | AProjLoans of symbolic_value * (msymbolic_value * aproj) list
       (** A projector of loans over a symbolic value.
       
           Note that the borrows of a symbolic value may be spread between
@@ -285,8 +285,6 @@ type aproj =
           We can later end the projector of loans if `s@0` is not referenced
           anywhere in the context below a projector of borrows which intersects
           this projector of loans.
-          
-          TODO: we should use an msymbolic_value, not an mvalue
        *)
   | AProjBorrows of symbolic_value * rty
       (** Note that an AProjBorrows only operates on a value which is not below
@@ -296,14 +294,12 @@ type aproj =
           can't get updated/expanded: this means that we don't need to save
           any meta-value here.
        *)
-  | AEndedProjLoans of msymbolic_value * (mvalue * aproj) list
+  | AEndedProjLoans of msymbolic_value * (msymbolic_value * aproj) list
       (** An ended projector of loans over a symbolic value.
       
           See the explanations for [AProjLoans]
           
           Note that we keep the original symbolic value as a meta-value.
-
-          TODO: we should use an msymbolic_value, not an mvalue
        *)
   | AEndedProjBorrows of mvalue
       (** The only purpose of [AEndedProjBorrows] is to store, for synthesis
-- 
cgit v1.2.3