aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetWeakList.v
blob: 9dbea8849594e01b40336f61d935ab35daca4c0a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(** * Finite sets library *)

(** This file proposes an implementation of the non-dependent
    interface [FSetInterface.WS] using lists without redundancy. *)

Require Import FSetInterface.
Set Implicit Arguments.
Unset Strict Implicit.

(** This is just a compatibility layer, the real implementation
    is now in [MSetWeakList] *)

Require Equalities FSetCompat MSetWeakList.

Module Make (X: DecidableType) <: WS with Module E := X.
 Module E := X.
 Module X' := Equalities.Update_DT X.
 Module MSet := MSetWeakList.Make X'.
 Include FSetCompat.Backport_WSets X MSet.
End Make.