diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1844.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1844.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v index 545f2615..5627612f 100644 --- a/test-suite/bugs/closed/shouldsucceed/1844.v +++ b/test-suite/bugs/closed/shouldsucceed/1844.v @@ -188,7 +188,7 @@ with exec_finish: function -> outcome -> store -> value -> store -> Prop := with exec_function: function -> store -> value -> store -> Prop := | exec_function_intro: forall f st out st1 v st', - exec f.(fn_body) st out st1 -> + exec f.(fn_body) st out st1 -> exec_finish f out st1 v st' -> exec_function f st v st'. |