From 019a8f76f210c97b56db52964ff022f9e56aee4a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 8 Jul 2017 16:20:00 -0400 Subject: Fix Demo.v --- src/Demo.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. -- cgit v1.2.3