aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2141.v
blob: 22e33c8e81a2a85910d209182a4ac5ab255534fc (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
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 TestCompile NatSet'.fold.

(* Extraction "test2141.ml" NatSet'.fold. *)