diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-06 13:35:21 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-06 13:35:21 +0100 |
| commit | eafd62f89435eddafdb7bfab3f33a888a84e8608 (patch) | |
| tree | 5839d4ce18b0665843983a691dd0a8ce8be353e0 /src/hls/HTLgenproof.v | |
| parent | 4d7236541250808487820beec0b3f79ac2a901dc (diff) | |
| download | vericert-eafd62f89435eddafdb7bfab3f33a888a84e8608.tar.gz vericert-eafd62f89435eddafdb7bfab3f33a888a84e8608.zip | |
Get HTLgenproof passing with updated spec
Diffstat (limited to 'src/hls/HTLgenproof.v')
| -rw-r--r-- | src/hls/HTLgenproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index eb7326a..53dbdb5 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -386,9 +386,9 @@ Ltac not_control_reg := solve [ unfold Ple, Plt in *; try multimatch goal with - | [ H : forall r, (exists x, _ ! r = Some x) -> (_ < r < _)%positive + | [ H : forall r, (exists x, _ ! r = Some x) -> (r > _)%positive |- context[?r'] - ] => destruct (H r' ltac:(eauto)) + ] => pose proof (H r' ltac:(eauto)) end; lia ]. @@ -467,7 +467,7 @@ Section CORRECTNESS. Lemma TRANSL' : Linking.match_program (fun cu f tf => transl_fundef prog f = Errors.OK tf) eq prog tprog. - Proof. intros; apply match_prog_matches; assumption. Qed. + Proof. pose proof match_prog_matches as H. unfold match_prog' in H. auto. Qed. Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. |