From cf19dd40f466691d28f4dfd86211724b700aa217 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Thu, 2 Jul 2020 16:38:23 +0100 Subject: Fix callstate proof. --- src/translation/HTLgenproof.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'src/translation/HTLgenproof.v') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 9b61b27..e4bbb8f 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -2023,9 +2023,9 @@ Section CORRECTNESS. unfold Mem.load. intros. match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H3. - unfold Mem.perm in H3. crush. - unfold Mem.perm_order' in H3. + invert v0. unfold Mem.range_perm in H4. + unfold Mem.perm in H4. crush. + unfold Mem.perm_order' in H4. small_tac. exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. rewrite Maps.PMap.gss in H8. @@ -2039,11 +2039,11 @@ Section CORRECTNESS. unfold Mem.store. intros. match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H3. - unfold Mem.perm in H3. crush. - unfold Mem.perm_order' in H3. + invert v0. unfold Mem.range_perm in H4. + unfold Mem.perm in H4. crush. + unfold Mem.perm_order' in H4. small_tac. - exploit (H3 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. + exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. rewrite Maps.PMap.gss in H8. match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. crush. -- cgit