diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-03-30 18:30:29 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-03-30 18:30:29 -0400 |
| commit | ce1a0e8508f53481138362f14581193b7394552b (patch) | |
| tree | 18f27142e59fbf2a006500db8280d9ddcfbc8669 /src/Util/ListUtil.v | |
| parent | 019c80c66cd4da0f7e3f6469bf1fe3ede11c7a12 (diff) | |
| parent | d819eeb7bd87746b62f6a6398f6ad69edb89a5ff (diff) | |
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 783e3f527..1f9a62457 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1,7 +1,7 @@ -Require Import List. -Require Import Omega. -Require Import Arith.Peano_dec. -Require Import VerdiTactics. +Require Import Coq.Lists.List. +Require Import Coq.omega.Omega. +Require Import Coq.Arith.Peano_dec. +Require Import Crypto.Tactics.VerdiTactics. Ltac boring := simpl; intuition; |