diff options
Diffstat (limited to 'src/translation/HTLgenproof.v')
| -rw-r--r-- | src/translation/HTLgenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index f07403d..77bd4ef 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -1424,7 +1424,7 @@ Section CORRECTNESS. assert (Some (AST.Internal x) = Some (AST.Internal m)). replace (AST.fundef HTL.module) with (HTL.fundef). rewrite <- H6. setoid_rewrite <- A. trivial. - trivial. inversion H7. + trivial. inv H7. assumption. Qed. Hint Resolve transl_initial_states : htlproof. |