diff options
| author | Son Ho | 2022-01-25 23:11:05 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-25 23:11:05 +0100 |
| commit | 592a2113734078290d4406df7804bfc128865958 (patch) | |
| tree | 015864f2dbf6f09ec1ac243d95e1818292608cd4 /src/Values.ml | |
| parent | 0a93309c8dc40fcda0bfb7f72bb8af38fcc14afd (diff) | |
Use msymbolic_value instead of mvalue in some places in Values.aproj
Diffstat (limited to '')
| -rw-r--r-- | src/Values.ml | 8 |
1 files changed, 2 insertions, 6 deletions
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 |