blob: 098a7e9e725fde1dc1439d1bf5422c2a416b8752 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Require Coq.extraction.Extraction.
Require Import FSetList.
Require Import OrderedTypeEx.
Module NatSet := FSetList.Make (Nat_as_OT).
Recursive Extraction NatSet.fold.
Module FSetHide (X : FSetInterface.S).
Include X.
End FSetHide.
Module NatSet' := FSetHide NatSet.
Recursive Extraction NatSet'.fold.
(* Extraction "test2141.ml" NatSet'.fold. *)
|
