diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-20 04:16:04 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-20 04:16:04 -0400 |
| commit | 8d498c587aaa23dcb50c31fa5a426873b3dd9dea (patch) | |
| tree | cb35e0b0a3a78a5028683bca952b1490d0f4fdbd | |
| parent | 87eb483a73bd2af1ab9a989e9002c1093988d927 (diff) | |
move nsatz into tactics directory
| -rw-r--r-- | _CoqProject | 2 | ||||
| -rw-r--r-- | src/Algebra.v | 4 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 2 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 4 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 2 | ||||
| -rw-r--r-- | src/Tactics/Nsatz.v (renamed from src/Nsatz.v) | 0 |
6 files changed, 7 insertions, 7 deletions
diff --git a/_CoqProject b/_CoqProject index 14179cb3d..9c4cdd3cf 100644 --- a/_CoqProject +++ b/_CoqProject @@ -5,7 +5,6 @@ Bedrock/Word.v src/Algebra.v src/BaseSystem.v src/BaseSystemProofs.v -src/Nsatz.v src/Testbit.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -34,6 +33,7 @@ src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v src/Specific/GF1305.v src/Specific/GF25519.v +src/Tactics/Nsatz.v src/Tactics/VerdiTactics.v src/Util/CaseUtil.v src/Util/IterAssocOp.v diff --git a/src/Algebra.v b/src/Algebra.v index 27c0d2e59..a319d0e80 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1,5 +1,5 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Crypto.Util.Tactics Crypto.Nsatz. +Require Import Crypto.Util.Tactics Crypto.Tactics.Nsatz. Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope. Section Algebra. @@ -591,4 +591,4 @@ Section Z. Example _example_nonzero_nsatz_contradict_Z x y : Z.mul x y = (Zpos xH) -> not (x = Z0). Proof. intros. intro. nsatz_contradict. Qed. -End Z.
\ No newline at end of file +End Z. diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index f9a866acb..89984027f 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -1,6 +1,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Algebra Crypto.Nsatz. +Require Import Crypto.Algebra Crypto.Tactics.Nsatz. Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index fe0e732a8..49c5d5041 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -1,6 +1,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Algebra Crypto.Nsatz. +Require Import Crypto.Algebra Crypto.Tactics.Nsatz. Require Import Crypto.CompleteEdwardsCurve.Pre Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. @@ -241,4 +241,4 @@ Module Extended. end. Qed. End Homomorphism. -End Extended.
\ No newline at end of file +End Extended. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 4744afe6b..397a6259c 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,5 +1,5 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Crypto.Algebra Crypto.Nsatz. +Require Import Crypto.Algebra Crypto.Tactics.Nsatz. Generalizable All Variables. Section Pre. diff --git a/src/Nsatz.v b/src/Tactics/Nsatz.v index 469ba4c29..469ba4c29 100644 --- a/src/Nsatz.v +++ b/src/Tactics/Nsatz.v |