diff options
Diffstat (limited to 'lib/HashedSet.v')
| -rw-r--r-- | lib/HashedSet.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/lib/HashedSet.v b/lib/HashedSet.v index 00074a43..6130ba17 100644 --- a/lib/HashedSet.v +++ b/lib/HashedSet.v @@ -1383,3 +1383,9 @@ Proof. apply WR.gfilter. Qed. End PSet. + +Require Extraction. + +Extract Inductive PSet.WR.pset => "HashedSetaux.pset" [ "HashedSetaux.empty" "HashedSetaux.node" ] "HashedSetaux.pset_match". + +Extract Inlined Constant PSet.WR.pset_eq => "HashedSetaux.eq". |