From afab285a4335bd59b23bba6bc0db684f96f9c5be Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Oct 2016 16:46:43 -0400 Subject: Fix for missing Nat.log2 in 8.4 --- src/BoundedArithmetic/X86ToZLikeProofs.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/BoundedArithmetic') diff --git a/src/BoundedArithmetic/X86ToZLikeProofs.v b/src/BoundedArithmetic/X86ToZLikeProofs.v index ef7067419..58d2bbfff 100644 --- a/src/BoundedArithmetic/X86ToZLikeProofs.v +++ b/src/BoundedArithmetic/X86ToZLikeProofs.v @@ -16,6 +16,7 @@ Require Import Crypto.ModularArithmetic.ZBounded. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.ZUtil Crypto.Util.Tactics. Require Import Crypto.Util.LetIn. +Import NPeano. Local Open Scope Z_scope. Local Coercion Z.of_nat : nat >-> Z. @@ -76,7 +77,7 @@ Section x86_gen_barrett_foundation. end. Local Ltac post_t := repeat post_t_step. Axiom proof_admitted : False. - Local Ltac admit := abstract case proof_admitted. + Tactic Notation "admit" := abstract case proof_admitted. Local Ltac t := admit; pre_t; post_t. Global Instance ZLikeProperties_of_x86_gen_Factored -- cgit v1.2.3