diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-06 15:34:06 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-06 15:34:06 +0100 |
| commit | bad5c59b014a9baf18df0e2146edcb11fb931216 (patch) | |
| tree | 7e80ac0bb3bdeda4ce662f3dcd4d7f148773e2c7 /src/hls/GiblePargenproof.v | |
| parent | 4290ead0dfdda0400dae528b66a38fe39dbbb18e (diff) | |
| download | vericert-bad5c59b014a9baf18df0e2146edcb11fb931216.tar.gz vericert-bad5c59b014a9baf18df0e2146edcb11fb931216.zip | |
Add assumption and prove assumption that preds are evaluable
Diffstat (limited to 'src/hls/GiblePargenproof.v')
| -rw-r--r-- | src/hls/GiblePargenproof.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index c48e5f3..0b9bd78 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -2380,6 +2380,7 @@ square: exploit abstr_sequence_correct; eauto; simplify. exploit local_abstr_check_correct2; eauto. { constructor. eapply ge_preserved_refl. reflexivity. } + { inv H. inv H8. exists pr'. intros x0. specialize (H x0). auto. } simplify. exploit abstr_seq_reverse_correct; eauto. reflexivity. simplify. exploit seqbb_step_parbb_step; eauto; intros. |