From eafd62f89435eddafdb7bfab3f33a888a84e8608 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Fri, 6 Aug 2021 13:35:21 +0100 Subject: Get HTLgenproof passing with updated spec --- src/hls/HTLgenproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/hls') 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. -- cgit