diff options
Diffstat (limited to 'contrib/subtac/test')
| -rw-r--r-- | contrib/subtac/test/take.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v index 968ab3ad77..07f63a2ba8 100644 --- a/contrib/subtac/test/take.v +++ b/contrib/subtac/test/take.v @@ -1,7 +1,7 @@ Variable A : Set. Require Import JMeq. Require Import List. - +Require Import Coq.subtac.Utils. Program Fixpoint take (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } := match n with |