cleanup

mit-plv · Jan 9, 2025 · b2d1b5c · b2d1b5c
1 parent 7d40f6c
commit b2d1b5c
Showing 1 changed file with 10 additions and 10 deletions.
diff --git 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.