diff options
Diffstat (limited to 'cfrontend/Initializersproof.v')
| -rw-r--r-- | cfrontend/Initializersproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 4d287bc..057933e 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -445,7 +445,7 @@ Proof. (* val *) destruct v; monadInv CV; constructor. (* rval *) - inv H1; rewrite H2 in CV; try congruence. eauto. + inv H1; rewrite H2 in CV; try congruence. eauto. eauto. (* addrof *) eauto. (* unop *) |