diff options
Diffstat (limited to 'src/hls/DVeriloggenproof.v')
| -rw-r--r-- | src/hls/DVeriloggenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/DVeriloggenproof.v b/src/hls/DVeriloggenproof.v index 31cdfca..197d9a6 100644 --- a/src/hls/DVeriloggenproof.v +++ b/src/hls/DVeriloggenproof.v @@ -501,7 +501,7 @@ Section CORRECTNESS. (* repeat rewrite_eq. apply match_state. assumption. *) (* - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. *) (* repeat rewrite_eq. apply match_state. assumption. *) - (* Qed. *) Admitted. + (* Qed. *) Admitted. (* This translation pass is only used for testing. *) #[local] Hint Resolve transl_step_correct : verilogproof. Lemma transl_initial_states : |