src/ulib/tests/examples: remove unused opens

mtzguido · mtzguido · commit 8e2665003141 · 2026-05-02T19:11:47.000-07:00
diff --git a/examples/layeredeffects/SimpleHeap.fst b/examples/layeredeffects/SimpleHeap.fst
@@ -3,7 +3,6 @@
 *)
 module SimpleHeap
 
-module S = FStar.Set
 module F = FStar.FunctionalExtensionality
 
 (** Internal cell type: stores a typed value *)
diff --git a/examples/layeredeffects/SimpleHeap.fsti b/examples/layeredeffects/SimpleHeap.fsti
@@ -7,7 +7,6 @@
 module SimpleHeap
 
 module S = FStar.Set
-module F = FStar.FunctionalExtensionality
 
 (** The heap type *)
 val heap : Type u#1
diff --git a/pulse/share/pulse/examples/EqualOrDisjoint.fst b/pulse/share/pulse/examples/EqualOrDisjoint.fst
@@ -1,8 +1,6 @@
 module EqualOrDisjoint
 #lang-pulse
 open Pulse.Lib.Pervasives
-module R = Pulse.Lib.Reference
-module TR = Pulse.Lib.Trade
 open Pulse.Lib.Trade
 open Pulse.Lib.Forall.Util
 
diff --git a/pulse/share/pulse/examples/Quicksort.Base.fst b/pulse/share/pulse/examples/Quicksort.Base.fst
@@ -19,7 +19,6 @@ module Quicksort.Base
 
 open Pulse.Lib.Pervasives
 module A = Pulse.Lib.Array
-module R = Pulse.Lib.Reference
 module SZ = FStar.SizeT
 (* Base module with proof of correctness of Quicksort, partition, etc.
 #lang-pulse
diff --git a/pulse/share/pulse/examples/by-example/PulseByExample.fst b/pulse/share/pulse/examples/by-example/PulseByExample.fst
@@ -49,7 +49,6 @@ fn five_alt ()
 
 open Pulse.Lib.Reference
 open Pulse.Class.PtsTo
-module R = Pulse.Lib.Reference
 
 (* 
   Things to note:
@@ -114,7 +113,6 @@ fn test (r:ref int)
 }
 
 open Pulse.Lib.Array
-module A = Pulse.Lib.Array
 module SZ = FStar.SizeT
 open Pulse.Lib.BoundedIntegers
 
diff --git a/pulse/share/pulse/examples/by-example/PulseTutorial.AtomicsAndInvariants.fst b/pulse/share/pulse/examples/by-example/PulseTutorial.AtomicsAndInvariants.fst
@@ -17,7 +17,6 @@
 module PulseTutorial.AtomicsAndInvariants
 #lang-pulse
 open Pulse.Lib.Pervasives
-module T = FStar.Tactics
 module U32 = FStar.UInt32
 
 //owns$
diff --git a/pulse/share/pulse/examples/parallel/Example.SimpleDBModel.fst b/pulse/share/pulse/examples/parallel/Example.SimpleDBModel.fst
@@ -3,7 +3,6 @@ module Example.SimpleDBModel
 open Pulse.Lib.Pervasives
 open Pulse.Lib.GhostPCMReference
 open FStar.Preorder
-module GR = Pulse.Lib.GhostPCMReference
 module MR = Pulse.Lib.MonotonicGhostRef
 let as_prop (p:prop) = p <==> True
 // A tiny db
diff --git a/pulse/src/checker/Pulse.Checker.Match.fst b/pulse/src/checker/Pulse.Checker.Match.fst
@@ -28,7 +28,6 @@ module T = FStar.Tactics.V2
 module L = FStar.List.Tot.Base
 module R = FStar.Reflection.V2
 module RT = FStar.Reflection.Typing
-module RU = Pulse.RuntimeUtils
 
 let br_typing_vis (g:env) (_:universe) (_:typ) (_:term) (_:pattern) (_:st_term) (_:comp_st) : Type = unit
 
diff --git a/src/smtencoding/FStarC.SMTEncoding.Encode.fsti b/src/smtencoding/FStarC.SMTEncoding.Encode.fsti
@@ -36,4 +36,4 @@ val encode_query: option (unit -> ML string)
                 -> ML (list decl  //prelude, translation of tcenv
                   & list ErrorReporting.label //labels in the query
                   & decl        //the query itself
-                  & list decl)  //suffix, evaluating labels in the model, etc
+                  & list decl)  //suffix, evaluating labels in the model, etc
diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fst b/src/typechecker/FStarC.TypeChecker.Normalize.fst
@@ -45,7 +45,6 @@ module PC = FStarC.Parser.Const
 module U  = FStarC.Syntax.Util
 module EMB = FStarC.Syntax.Embeddings
 module TcComm = FStarC.TypeChecker.Common
-module TEQ = FStarC.TypeChecker.TermEqAndSimplify
 module PO = FStarC.TypeChecker.Primops
 module Print = FStarC.Syntax.Print //bring into scope for show instances
 open FStarC.TypeChecker.Normalize.Unfolding
diff --git a/src/typechecker/FStarC.TypeChecker.TcEffect.fst b/src/typechecker/FStarC.TypeChecker.TcEffect.fst
@@ -37,7 +37,6 @@ module TcUtil = FStarC.TypeChecker.Util
 module Gen = FStarC.TypeChecker.Generalize
 module TEQ = FStarC.TypeChecker.TermEqAndSimplify
 
-module BU = FStarC.Util
 open FStarC.Class.Show
 open FStarC.Class.Tagged
 
diff --git a/tests/bug-reports/closed/Bug2069.fst b/tests/bug-reports/closed/Bug2069.fst
@@ -1,5 +1,4 @@
 module Bug2069
-module WF = FStar.WellFounded
 
 
 let id (a : Type u#aa) (x:a) : a = x
diff --git a/tests/machine_integers/TestRotate.fst b/tests/machine_integers/TestRotate.fst
@@ -4,10 +4,8 @@ open FStar.All
 open FStar.IO
 
 module U8   = FStar.UInt8
-module U16  = FStar.UInt16
 module U32  = FStar.UInt32
 module U64  = FStar.UInt64
-module I8   = FStar.Int8
 module I32  = FStar.Int32
 
 let check s (b:bool) : ML unit =
diff --git a/ulib/FStar.Injection.fsti b/ulib/FStar.Injection.fsti
@@ -2,7 +2,6 @@ module FStar.Injection
 
 open FStar.Fin
 open FStar.Functions
-module SZ = FStar.SizeT
 open FStar.SizeT { (/^), (%^), (+^), (-^), ( *^ )  }
 open FStar.Tactics.Easy
 
