diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-05 16:34:40 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-05 16:34:40 +0100 |
| commit | ad16b6526aa5ccbb895053e59bf03ba19beedbad (patch) | |
| tree | d5a0b5d4d869e2665e3d279a45c75a3fa73e177f /lib | |
| parent | b6c4a550705b36254aab812efd7b256e3cea7b51 (diff) | |
| download | compcert-kvx-ad16b6526aa5ccbb895053e59bf03ba19beedbad.tar.gz compcert-kvx-ad16b6526aa5ccbb895053e59bf03ba19beedbad.zip | |
HashedSet with extraction
Diffstat (limited to 'lib')
| -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". |