diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-10-11 16:39:13 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-10-11 16:39:13 +0100 |
| commit | f8bd8cde25321a3a4a3195bf9189416194b3732e (patch) | |
| tree | 7773d41eebb8ad6e26d545cc81ad51d24d2bd6a4 /src/hls/GibleSeq.v | |
| parent | c35404c110b7616b30eeb48fc4051dcb33d84f40 (diff) | |
| download | vericert-f8bd8cde25321a3a4a3195bf9189416194b3732e.tar.gz vericert-f8bd8cde25321a3a4a3195bf9189416194b3732e.zip | |
Clean up proofs
Diffstat (limited to 'src/hls/GibleSeq.v')
| -rw-r--r-- | src/hls/GibleSeq.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v index 793eb5d..4bb001b 100644 --- a/src/hls/GibleSeq.v +++ b/src/hls/GibleSeq.v @@ -143,7 +143,7 @@ Proof. exists x. exists (a :: x0). exists x1. simplify; auto. econstructor; eauto. - inv H3. - exists p. exists nil. exists bb. crush. + exists p. exists (@nil instr). exists bb. crush. constructor. Qed. |