prelude.v 278 Bytes
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
2
(* This file is distributed under the terms of the BSD license. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
3
Require Export
4 5
  base
  tactics
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8
  decidable
  orders
  option
9 10
  vector
  numbers
Robbert Krebbers's avatar
Robbert Krebbers committed
11
  ars
12 13 14
  collections
  fin_collections
  listset
15
  fresh_numbers
16 17
  list
  lexico.