diff options
Diffstat (limited to 'cfrontend/SimplLocalsproof.v')
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 552c991..ae98130 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -1710,12 +1710,12 @@ Inductive match_states: state -> state -> Prop := match_states (State f s k e le m) (State tf ts tk te tle tm) | match_call_state: - forall fd vargs k m tfd tvargs tk tm j targs tres + forall fd vargs k m tfd tvargs tk tm j targs tres cconv (TRFD: transf_fundef fd = OK tfd) (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm)) (MINJ: Mem.inject j m tm) (AINJ: val_list_inject j vargs tvargs) - (FUNTY: type_of_fundef fd = Tfunction targs tres) + (FUNTY: type_of_fundef fd = Tfunction targs tres cconv) (ANORM: val_casted_list vargs targs), match_states (Callstate fd vargs k m) (Callstate tfd tvargs tk tm) |