diff options
| -rw-r--r-- | cfrontend/SimplExpr.v | 1 | ||||
| -rw-r--r-- | cfrontend/SimplLocals.v | 1 | ||||
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 2 | ||||
| -rw-r--r-- | lib/Coqlib.v | 1 |
4 files changed, 4 insertions, 1 deletions
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 45b686f3..7cdff468 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -26,6 +26,7 @@ Require Import Csyntax. Require Import Clight. Local Open Scope string_scope. +Local Open Scope list_scope. (** State and error monad for generating fresh identifiers. *) diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index b142d3cc..f54aa60d 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -22,6 +22,7 @@ Require Compopts. Open Scope error_monad_scope. Open Scope string_scope. +Open Scope list_scope. Module VSet := FSetAVL.Make(OrderedPositive). diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 7af499f4..26d3d347 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -1053,7 +1053,7 @@ Proof. assert (RPSRC: Mem.range_perm m bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sizeof tge ty) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty). - replace (sizeof tge ty) with (Z.of_nat (length bytes)). + replace (sizeof tge ty) with (Z.of_nat (List.length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. rewrite LEN. apply nat_of_Z_eq. omega. assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty). diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 3fe1ea2e..3b8e5b3b 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -17,6 +17,7 @@ used throughout the development. It complements the Coq standard library. *) +Require Export String. Require Export ZArith. Require Export Znumtheory. Require Export List. |