diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-11 16:46:43 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-11 16:46:43 -0400 |
| commit | afab285a4335bd59b23bba6bc0db684f96f9c5be (patch) | |
| tree | 187bc54d3c4c226ffb8e2fdfe97a5c2e42eae801 /src/BoundedArithmetic | |
| parent | 36ab9b2519271f9596f0de69df9af3e2ff1b3ed8 (diff) | |
Fix for missing Nat.log2 in 8.4
Diffstat (limited to 'src/BoundedArithmetic')
| -rw-r--r-- | src/BoundedArithmetic/X86ToZLikeProofs.v | 3 |
1 files changed, 2 insertions, 1 deletions
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 |