aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-19 13:24:16 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-22 15:29:20 +0200
commit107ef2db28b7abc75afe32350e7c2eb3c8ddbe82 (patch)
treeeab54255977164228c3ae2c8a07dc3f2099491c6 /plugins/omega
parent16a505cd851ef5f3a151d08af5397da97b4d2943 (diff)
refl_omega: some code refactoring
Diffstat (limited to 'plugins/omega')
-rw-r--r--plugins/omega/omega.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index f655c176f..2a018fa3f 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -96,7 +96,7 @@ type afine = {
type state_action = {
st_new_eq : afine;
- st_def : afine;
+ st_def : afine; (* /!\ this represents [st_def = st_var] *)
st_orig : afine;
st_coef : bigint;
st_var : int }