diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-25 09:09:23 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-25 09:09:23 +0100 |
| commit | 445aabbcf63e29d68dd0c98dde7f259af0381591 (patch) | |
| tree | fe77b0b489849e60dca1fc221f7c3a301ec776e5 /src/translation/HTLgenproof.v | |
| parent | 14cd3b8b12e3db17c3842ae9dfdb30ca86b6394c (diff) | |
| download | vericert-kvx-445aabbcf63e29d68dd0c98dde7f259af0381591.tar.gz vericert-kvx-445aabbcf63e29d68dd0c98dde7f259af0381591.zip | |
Work on Veriloggen proof
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. |