From b2d1b5cd26b3db57b79a1734d0f2a5f1baa70409 Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Thu, 9 Jan 2025 13:45:33 -0500 Subject: [PATCH] cleanup --- bedrock2/src/bedrock2/FE310CSemantics.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/bedrock2/src/bedrock2/FE310CSemantics.v b/bedrock2/src/bedrock2/FE310CSemantics.v index d01e48168..de7523fae 100644 --- a/bedrock2/src/bedrock2/FE310CSemantics.v +++ b/bedrock2/src/bedrock2/FE310CSemantics.v @@ -49,16 +49,16 @@ Section WithParameters. intros. all : repeat match goal with - | H : context[(?x =? ?y)%string] |- _ => - destruct (x =? y)%string in * - | H: exists _, _ |- _ => destruct H - | H: _ /\ _ |- _ => destruct H - | H: False |- _ => destruct H - end; subst; - repeat match goal with - | H: _ :: _ = _ :: _ |- _ => injection H; intros; subst; clear H - end; - eauto 8 using Properties.map.same_domain_refl. + | H : context[(?x =? ?y)%string] |- _ => + destruct (x =? y)%string in * + | H: exists _, _ |- _ => destruct H + | H: _ /\ _ |- _ => destruct H + | H: False |- _ => destruct H + end; subst; + repeat match goal with + | H: _ :: _ = _ :: _ |- _ => injection H; intros; subst; clear H + end; + eauto 8 using Properties.map.same_domain_refl. Qed. Global Instance ext_spec : Semantics.ExtSpec := deleakaged_ext_spec.