From f6f537dd60336b599c9541b0dca56255bdf2ba5e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 27 Aug 2018 11:13:47 -0400 Subject: Import prim token notations before using them This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. Closes #246 Closes #250 --- cfrontend/SimplExpr.v | 1 + cfrontend/SimplLocals.v | 1 + cfrontend/SimplLocalsproof.v | 2 +- lib/Coqlib.v | 1 + 4 files changed, 4 insertions(+), 1 deletion(-) 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. -- cgit