remove bedrock2.ptsto_bytes (#475)

Author: andres-erbsen

LiveVerif/src/LiveVerif/LiveProgramLogic.v

@@ -18,7 +18,7 @@ Require Import bedrock2.Syntax bedrock2.Semantics.
 Require Import bedrock2.Lift1Prop.
 Require Import bedrock2.Map.Separation bedrock2.Map.SeparationLogic bedrock2.Array.
 Require Import bedrock2.unzify.
-Require Import bedrock2.ptsto_bytes bedrock2.Scalars.
+Require Import bedrock2.Scalars.
 Require Import bedrock2.TacticError. Local Open Scope Z_scope.
 Require Import bedrock2.SuppressibleWarnings.
 Require Import LiveVerif.string_to_ident.

LiveVerif/src/LiveVerif/LiveVerifLib.v

@@ -13,7 +13,7 @@ Require Export bedrock2.Lift1Prop.
 Require Export bedrock2.Map.Separation bedrock2.Map.SeparationLogic.
 Require Export bedrock2.Map.DisjointUnion.
 Require Export bedrock2.unzify.
-Require Export bedrock2.ptsto_bytes bedrock2.Scalars.
+Require Export bedrock2.Scalars.
 Require Export coqutil.Word.Bitwidth.
 Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListString.
 Require Export bedrock2.SepBulletPoints.

LiveVerif/src/LiveVerif/PackageContext.v

@@ -15,7 +15,7 @@ Require Import bedrock2.Syntax bedrock2.Semantics.
 Require Import bedrock2.Lift1Prop.
 Require Import bedrock2.Map.Separation bedrock2.Map.SeparationLogic bedrock2.Array.
 Require Import bedrock2.groundcbv.
-Require Import bedrock2.ptsto_bytes bedrock2.Scalars.
+Require Import bedrock2.Scalars.
 Require Import bedrock2.TacticError. Local Open Scope Z_scope.
 Require Import LiveVerif.string_to_ident.
 Require Import bedrock2.ident_to_string.

bedrock2/src/bedrock2/ptsto_bytes.v

@@ -37,7 +37,6 @@ Require Import compiler.SeparationLogic.
 Require Import bedrock2.Scalars.
 Require Import coqutil.Tactics.Simp.
 Require Export coqutil.Word.SimplWordExpr.
-Require Import bedrock2.ptsto_bytes.
 Require Import compiler.RiscvWordProperties.
 Require Import compiler.eqexact.
 Require Import compiler.on_hyp_containing.

compiler/src/compiler/FlatToRiscvCommon.v

@@ -1,6 +1,5 @@
 Require Import Coq.Arith.Arith.
 Require Import bedrock2.Map.SeparationLogic.
-Require Import bedrock2.ptsto_bytes.
 Require Import coqutil.Decidable.
 Require Import coqutil.Word.Properties.
 Require Import compiler.ExprImp.