diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-09 16:41:41 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-07-11 09:59:13 -0400 |
| commit | 0cdb6bb7bcefc7c2f6e08123e40a54cca040de77 (patch) | |
| tree | b14e6bd7a5b396dbda10ac2406600c45aca85eb2 /src/WeierstrassCurve/Pre.v | |
| parent | 81dbc4239ed962affea9bf3918b9619b525ecdc0 (diff) | |
port CompleteEdwardsCurveTheorems (builds again)
Diffstat (limited to 'src/WeierstrassCurve/Pre.v')
| -rw-r--r-- | src/WeierstrassCurve/Pre.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v index 060d2f479..71a970b7d 100644 --- a/src/WeierstrassCurve/Pre.v +++ b/src/WeierstrassCurve/Pre.v @@ -1,5 +1,5 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Algebra. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. |