Commit 7d49702c authored by Robbert Krebbers's avatar Robbert Krebbers

Clean up imports in `infinite` file.

parent 17f8c792
(* Copyright (c) 2012-2019, Coq-std++ developers. *) (* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
From stdpp Require Import pretty fin_collections relations prelude gmap. From stdpp Require Export fin_collections.
From stdpp Require Import pretty relations.
(** The class [Infinite] axiomatizes types with infinitely many elements (** The class [Infinite] axiomatizes types with infinitely many elements
by giving an injection from the natural numbers into the type. It is mostly by giving an injection from the natural numbers into the type. It is mostly
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment