From b800fea5be9fc9f50bbcfe346f0737d4e2efc44f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 14 Mar 2019 15:46:33 +0100
Subject: [PATCH] Update tagset for FSet renaming

---
 examples/stdlib/tagset/why3session.xml | 204 ++++++++++++-------------
 stdlib/mach/tagset.mlw                 |  18 +--
 2 files changed, 111 insertions(+), 111 deletions(-)

diff --git a/examples/stdlib/tagset/why3session.xml b/examples/stdlib/tagset/why3session.xml
index 30aa0f2fb..1b8ec3055 100644
--- a/examples/stdlib/tagset/why3session.xml
+++ b/examples/stdlib/tagset/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -22,333 +22,333 @@
 </theory>
 <theory name="TagSet" proved="true">
  <goal name="VC iteration_state" expl="VC for iteration_state" proved="true">
- <proof prover="1"><result status="valid" time="0.61"/></proof>
+ <proof prover="1"><result status="valid" time="0.07"/></proof>
  </goal>
  <goal name="VC t" expl="VC for t" proved="true">
- <proof prover="1"><result status="valid" time="0.23"/></proof>
+ <proof prover="1"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC create" expl="VC for create" proved="true">
- <proof prover="1"><result status="valid" time="0.66"/></proof>
+ <proof prover="1"><result status="valid" time="0.09"/></proof>
  </goal>
  <goal name="VC mem" expl="VC for mem" proved="true">
- <proof prover="1"><result status="valid" time="0.68"/></proof>
+ <proof prover="1"><result status="valid" time="0.11"/></proof>
  </goal>
  <goal name="VC max_tags" expl="VC for max_tags" proved="true">
- <proof prover="1"><result status="valid" time="0.60"/></proof>
+ <proof prover="1"><result status="valid" time="0.09"/></proof>
  </goal>
  <goal name="VC resize" expl="VC for resize" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="VC resize.0" expl="integer overflow" proved="true">
-  <proof prover="1"><result status="valid" time="0.38"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="VC resize.1" expl="division by zero" proved="true">
-  <proof prover="1"><result status="valid" time="0.28"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC resize.2" expl="integer overflow" proved="true">
-  <proof prover="1"><result status="valid" time="0.50"/></proof>
+  <proof prover="1"><result status="valid" time="0.07"/></proof>
   </goal>
   <goal name="VC resize.3" expl="integer overflow" proved="true">
-  <proof prover="1"><result status="valid" time="0.50"/></proof>
+  <proof prover="1"><result status="valid" time="0.07"/></proof>
   </goal>
   <goal name="VC resize.4" expl="array creation size" proved="true">
-  <proof prover="1"><result status="valid" time="0.40"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC resize.5" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.39"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="VC resize.6" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.28"/></proof>
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC resize.7" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.35"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC resize.8" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.47"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC resize.9" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.64"/></proof>
+  <proof prover="1"><result status="valid" time="0.10"/></proof>
   </goal>
   <goal name="VC resize.10" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.60"/></proof>
+  <proof prover="1"><result status="valid" time="0.10"/></proof>
   </goal>
   <goal name="VC resize.11" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.62"/></proof>
+  <proof prover="1"><result status="valid" time="0.09"/></proof>
   </goal>
   <goal name="VC resize.12" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.64"/></proof>
+  <proof prover="1"><result status="valid" time="0.11"/></proof>
   </goal>
   <goal name="VC resize.13" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.35"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC resize.14" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.35"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="VC resize.15" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.30"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="VC add" expl="VC for add" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="VC add.0" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.25"/></proof>
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC add.1" expl="index in array bounds" proved="true">
-  <proof prover="1"><result status="valid" time="0.26"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC add.2" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.26"/></proof>
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC add.3" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.31"/></proof>
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC add.4" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.30"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC add.5" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.35"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC add.6" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.27"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC add.7" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.24"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC add.8" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.23"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC add.9" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.45"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC add.10" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.62"/></proof>
+  <proof prover="1"><result status="valid" time="0.10"/></proof>
   </goal>
   <goal name="VC add.11" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.63"/></proof>
+  <proof prover="1"><result status="valid" time="0.10"/></proof>
   </goal>
   <goal name="VC add.12" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.78"/></proof>
+  <proof prover="1"><result status="valid" time="0.11"/></proof>
   </goal>
   <goal name="VC add.13" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.71"/></proof>
+  <proof prover="1"><result status="valid" time="0.15"/></proof>
   </goal>
   <goal name="VC add.14" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.32"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="VC add.15" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.32"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="VC remove" expl="VC for remove" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="VC remove.0" expl="index in array bounds" proved="true">
-  <proof prover="1"><result status="valid" time="0.28"/></proof>
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC remove.1" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.26"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.2" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.37"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC remove.3" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.32"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.4" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.29"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.5" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.27"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.6" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.22"/></proof>
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC remove.7" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.24"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.8" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.44"/></proof>
+  <proof prover="1"><result status="valid" time="0.07"/></proof>
   </goal>
   <goal name="VC remove.9" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.62"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC remove.10" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.60"/></proof>
+  <proof prover="1"><result status="valid" time="0.10"/></proof>
   </goal>
   <goal name="VC remove.11" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.71"/></proof>
+  <proof prover="1"><result status="valid" time="0.10"/></proof>
   </goal>
   <goal name="VC remove.12" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.68"/></proof>
+  <proof prover="1"><result status="valid" time="0.13"/></proof>
   </goal>
   <goal name="VC remove.13" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.31"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC remove.14" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.81"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC remove.15" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.28"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC remove.16" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.27"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.17" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.27"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.18" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.26"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.19" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.31"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.20" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.24"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.21" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.22"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.22" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.38" steps="185"/></proof>
+  <proof prover="0"><result status="valid" time="0.05" steps="161"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="VC iterator" expl="VC for iterator" proved="true">
- <proof prover="1"><result status="valid" time="0.66"/></proof>
+ <proof prover="1"><result status="valid" time="0.11"/></proof>
  </goal>
  <goal name="Iterator.VC create" expl="VC for create" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="VC create.0" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.38"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC create.1" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.39"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC create.2" expl="index in array bounds" proved="true">
-  <proof prover="1"><result status="valid" time="0.24"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC create.3" expl="integer overflow" proved="true">
-  <proof prover="1"><result status="valid" time="0.39"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="VC create.4" expl="loop variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.32"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC create.5" expl="loop invariant preservation" proved="true">
-  <proof prover="1"><result status="valid" time="0.35"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="VC create.6" expl="loop invariant preservation" proved="true">
-  <proof prover="1"><result status="valid" time="0.47"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC create.7" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.48"/></proof>
+  <proof prover="1"><result status="valid" time="0.07"/></proof>
   </goal>
   <goal name="VC create.8" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.34"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC create.9" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.48"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC create.10" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.46"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC create.11" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.77"/></proof>
+  <proof prover="1"><result status="valid" time="0.13"/></proof>
   </goal>
   <goal name="VC create.12" expl="precondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="VC create.12.0" expl="precondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.27"/></proof>
+   <proof prover="1"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="VC create.12.1" expl="precondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="VC create.12.1.0" expl="precondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.42"/></proof>
+    <proof prover="1"><result status="valid" time="0.07"/></proof>
     </goal>
     <goal name="VC create.12.1.1" expl="precondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.40"/></proof>
+    <proof prover="1"><result status="valid" time="0.06"/></proof>
     </goal>
    </transf>
    </goal>
    <goal name="VC create.12.2" expl="precondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.60"/></proof>
+   <proof prover="1"><result status="valid" time="0.12"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="VC create.13" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.23"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC create.14" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.24"/></proof>
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC create.15" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.22"/></proof>
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="Iterator.VC is_empty" expl="VC for is_empty" proved="true">
- <proof prover="2"><result status="valid" time="0.82"/></proof>
+ <proof prover="2"><result status="valid" time="0.17"/></proof>
  </goal>
  <goal name="Iterator.VC next" expl="VC for next" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="VC next.0" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.14" steps="78"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
   </goal>
   <goal name="VC next.1" expl="index in array bounds" proved="true">
-  <proof prover="1"><result status="valid" time="0.41"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="VC next.2" expl="integer overflow" proved="true">
-  <proof prover="1"><result status="valid" time="0.44"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="VC next.3" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.32"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC next.4" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.39"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="VC next.5" expl="index in array bounds" proved="true">
-  <proof prover="1"><result status="valid" time="0.43"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC next.6" expl="integer overflow" proved="true">
-  <proof prover="1"><result status="valid" time="0.43"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="VC next.7" expl="loop variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.36"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC next.8" expl="loop invariant preservation" proved="true">
-  <proof prover="1"><result status="valid" time="0.34"/></proof>
+  <proof prover="1"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC next.9" expl="loop invariant preservation" proved="true">
-  <proof prover="1"><result status="valid" time="0.50"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC next.10" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.49"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC next.11" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.72"/></proof>
+  <proof prover="1"><result status="valid" time="0.12"/></proof>
   </goal>
   <goal name="VC next.12" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.51"/></proof>
+  <proof prover="1"><result status="valid" time="0.07"/></proof>
   </goal>
   <goal name="VC next.13" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.55"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC next.14" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.56"/></proof>
+  <proof prover="1"><result status="valid" time="0.09"/></proof>
   </goal>
   <goal name="VC next.15" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="1.58"/></proof>
+  <proof prover="1"><result status="valid" time="0.58"/></proof>
   </goal>
   <goal name="VC next.16" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.78"/></proof>
+  <proof prover="1"><result status="valid" time="0.13"/></proof>
   </goal>
   <goal name="VC next.17" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.68"/></proof>
+  <proof prover="1"><result status="valid" time="0.12"/></proof>
   </goal>
   <goal name="VC next.18" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.29"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC next.19" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.27"/></proof>
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
  </transf>
  </goal>
diff --git a/stdlib/mach/tagset.mlw b/stdlib/mach/tagset.mlw
index 06fba93df..1add3e7cb 100644
--- a/stdlib/mach/tagset.mlw
+++ b/stdlib/mach/tagset.mlw
@@ -35,7 +35,7 @@ module TagSetIntf
   type iteration_state = mutable { }
 
   type t = abstract {
-         mutable elts: S.set key;
+         mutable elts: S.fset key;
          mutable iterated: iteration_state;
        }
    invariant { not (S.mem S.dummy elts) }
@@ -66,9 +66,9 @@ module TagSetIntf
 
   type iterator = abstract {
        iterating: iteration_state;
-       mutable seen: S.set key;
-       mutable todo: S.set key;
-       all: S.set key;
+       mutable seen: S.fset key;
+       mutable todo: S.fset key;
+       all: S.fset key;
   }
   invariant { S.(union seen todo == all) }
   invariant { S.(inter seen todo == S.empty) }
@@ -118,7 +118,7 @@ module TagSet
   clone import S as S with axiom tag_correct
 
   type iteration_state = mutable {
-       ghost mutable elts': S.set key;
+       ghost mutable elts': S.fset key;
        mutable value: array key;
   }
   invariant { not (S.mem S.dummy elts') }
@@ -132,7 +132,7 @@ module TagSet
    }
 
   type t = {
-         ghost mutable elts: S.set key;
+         ghost mutable elts: S.fset key;
          mutable iterated: iteration_state;
        }
    invariant { elts = iterated.elts' }
@@ -204,9 +204,9 @@ module TagSet
 
   type iterator = {
        iterating: iteration_state;
-       ghost mutable seen: S.set key;
-       ghost mutable todo: S.set key;
-       ghost all: S.set key;
+       ghost mutable seen: S.fset key;
+       ghost mutable todo: S.fset key;
+       ghost all: S.fset key;
        mutable offset: int63;
   }
   invariant { S.(==) all (S.union seen todo) }
-- 
2.24.1