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/SimplLocalsproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend/SimplLocalsproof.v') 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). -- cgit