From 445aabbcf63e29d68dd0c98dde7f259af0381591 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 25 Jun 2020 09:09:23 +0100 Subject: Work on Veriloggen proof --- src/translation/HTLgenproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/translation/HTLgenproof.v') 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. -- cgit