diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-13 15:29:14 +0200 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-10-18 11:12:52 -0400 |
| commit | 94aff5d20480d1471d2520f690c5b5f7ffbf0aaf (patch) | |
| tree | ecf2a44eaec13e8615b20252cae9d77c56980490 /src/Util/AdditionChainExponentiation.v | |
| parent | 1636b6872b4947a238b433ad904899548ff8edfd (diff) | |
Add a Require Import FunInd (Function isn't loaded by default anymore)
See PR #220 https://github.com/coq/coq/pull/220
Diffstat (limited to 'src/Util/AdditionChainExponentiation.v')
| -rw-r--r-- | src/Util/AdditionChainExponentiation.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index 8de191eda..803cc85c6 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -1,3 +1,4 @@ +Require Import Coq.funind.FunInd. Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations. Require Import Coq.Numbers.BinNums Coq.NArith.BinNat. Require Import Crypto.Util.ListUtil. |