diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index de711045c2..69c3904c96 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -361,7 +361,7 @@ Variable e: env. Variable le: temp_env. Variable m: mem. -(** [eval_expr ge e m a v] defines the evaluation of expression [a] +(** [eval_expr ge e le m a v] defines the evaluation of expression [a] in r-value position. [v] is the value of the expression. [e] is the current environment and [m] is the current memory state. *)