From ad16b6526aa5ccbb895053e59bf03ba19beedbad Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 5 Mar 2020 16:34:40 +0100 Subject: HashedSet with extraction --- lib/HashedSet.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'lib/HashedSet.v') 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". -- cgit