diff options
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. |