diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-07-08 16:20:00 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-07-08 16:20:00 -0400 |
| commit | 019a8f76f210c97b56db52964ff022f9e56aee4a (patch) | |
| tree | 6ad215f72783954120477ee4b40f9ed177fecfdf /src/Demo.v | |
| parent | 59dec7e5b97b447e91a8d86440848f4c5d74c93f (diff) | |
Fix Demo.v
Diffstat (limited to 'src/Demo.v')
| -rw-r--r-- | src/Demo.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Demo.v b/src/Demo.v index 2011fcb0d..39b3f7501 100644 --- a/src/Demo.v +++ b/src/Demo.v @@ -1,6 +1,6 @@ (* Following http://adam.chlipala.net/theses/andreser.pdf chapter 3 *) Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. -Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable. +Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. |