Merge branch 'master' of gh:FStarLang/karamel

FStarLang · Feb 18, 2025 · 976b8a0 · 976b8a0
2 parents fa784c5 + cfddb06
commit 976b8a0
Show file tree

Hide file tree

Showing 29 changed files with 0 additions and 41 deletions.
diff --git a/krmllib/C.String.fst b/krmllib/C.String.fst
@@ -1,10 +1,7 @@
 module C.String
 
-module U8 = FStar.UInt8
 module U32 = FStar.UInt32
 
-module B = LowStar.Buffer
-module M = LowStar.Modifies
 
 open FStar.HyperStack.ST
 

diff --git a/krmllib/C.String.fsti b/krmllib/C.String.fsti
@@ -1,6 +1,5 @@
 module C.String
 
-module U8 = FStar.UInt8
 module U32 = FStar.UInt32
 
 module B = LowStar.Buffer

diff --git a/krmllib/C.fst b/krmllib/C.fst
@@ -2,7 +2,6 @@ module C
 
 open FStar.HyperStack.ST
 
-module HS = FStar.HyperStack
 module U8 = FStar.UInt8
 
 // This module contains a series of bindings that already exist in C. It receives

diff --git a/krmllib/LowStar.Lib.AssocList.fst b/krmllib/LowStar.Lib.AssocList.fst
@@ -5,8 +5,6 @@ module LowStar.Lib.AssocList
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
 module G = FStar.Ghost
-module L = FStar.List.Tot
-module U32 = FStar.UInt32
 module ST = FStar.HyperStack.ST
 
 module M = FStar.Map

diff --git a/krmllib/LowStar.Lib.AssocList.fsti b/krmllib/LowStar.Lib.AssocList.fsti
@@ -4,14 +4,9 @@ module LowStar.Lib.AssocList
 
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
-module G = FStar.Ghost
-module L = FStar.List.Tot
-module U32 = FStar.UInt32
 module ST = FStar.HyperStack.ST
 
 module M = FStar.Map
-module LL2 = LowStar.Lib.LinkedList2
-module LL1 = LowStar.Lib.LinkedList
 
 open FStar.HyperStack.ST
 open LowStar.BufferOps

diff --git a/krmllib/LowStar.Lib.LinkedList2.fst b/krmllib/LowStar.Lib.LinkedList2.fst
@@ -14,8 +14,6 @@ open LowStar.BufferOps
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
 module G = FStar.Ghost
-module L = FStar.List.Tot
-module U32 = FStar.UInt32
 module ST = FStar.HyperStack.ST
 
 module LL1 = LowStar.Lib.LinkedList

diff --git a/krmllib/TestLib.fsti b/krmllib/TestLib.fsti
@@ -3,7 +3,6 @@ module TestLib
 open FStar.HyperStack.ST
 open LowStar.Buffer
 
-module HS = FStar.HyperStack
 module Buffer = LowStar.Buffer
 
 (** Some test routines *)

diff --git a/krmllib/compat/C.Compat.String.fst b/krmllib/compat/C.Compat.String.fst
@@ -1,6 +1,5 @@
 module C.Compat.String
 
-module U8 = FStar.UInt8
 module U32 = FStar.UInt32
 
 module B = LowStar.Buffer

diff --git a/krmllib/compat/C.Compat.fst b/krmllib/compat/C.Compat.fst
@@ -2,7 +2,6 @@ module C.Compat
 
 open FStar.HyperStack.ST
 
-module HS = FStar.HyperStack
 module U8 = FStar.UInt8
 
 // This module contains a series of bindings that already exist in C. It receives

diff --git a/krmllib/compat/C.Nullity.fsti b/krmllib/compat/C.Nullity.fsti
@@ -37,9 +37,6 @@ let (!*) (#a: Type) (p: pointer a):
   (ensures (fun h0 x h1 -> B.live h1 p /\ x == B.get h0 p 0 /\ h1 == h0)) =
   B.index p 0ul
 
-module U32 = FStar.UInt32
-module Seq = FStar.Seq
-module Heap = FStar.Heap
 
 (* Two pointers with different reads are disjoint *)
 

diff --git a/test/Ctypes2.fst b/test/Ctypes2.fst
@@ -4,8 +4,6 @@ open FStar.Mul
 open FStar.UInt
 open FStar.HyperStack.ST
 
-module M = LowStar.Modifies
-module U16 = FStar.UInt16
 module U32 = FStar.UInt32
 
 open Ctypes1

diff --git a/test/Ctypes4.fst b/test/Ctypes4.fst
@@ -5,7 +5,6 @@ open FStar.UInt
 open FStar.HyperStack.ST
 
 module B = LowStar.Buffer
-module M = LowStar.Modifies
 module U16 = FStar.UInt16
 module U32 = FStar.UInt32
 module U128 = FStar.UInt128

diff --git a/test/DataTypesEq.fst b/test/DataTypesEq.fst
@@ -1,6 +1,5 @@
 module DataTypesEq
 
-module SoBuggy = FStar.HyperStack.ST
 
 type t =
   | A: UInt32.t -> t

diff --git a/test/HigherOrder2.fst b/test/HigherOrder2.fst
@@ -1,6 +1,5 @@
 module HigherOrder2
 
-module HS = FStar.HyperStack
 module HST = FStar.HyperStack.ST
 module I32 = FStar.Int32
 module M = LowStar.Modifies

diff --git a/test/HigherOrder4.fst b/test/HigherOrder4.fst
@@ -4,7 +4,6 @@ module B = LowStar.Buffer
 module HS = FStar.HyperStack
 module HST = FStar.HyperStack.ST
 module M = LowStar.Modifies
-module U32 = FStar.UInt32
 module I32 = FStar.Int32
 
 open LowStar.BufferOps

diff --git a/test/Layered.fst b/test/Layered.fst
@@ -1,7 +1,6 @@
 module Layered
 
 open FStar.HyperStack.ST
-module U32 = FStar.UInt32
 module HS = FStar.HyperStack
 
 inline_for_extraction

diff --git a/test/LinkedList1.fst b/test/LinkedList1.fst
@@ -1,6 +1,5 @@
 module LinkedList1
 
-module B = FStar.Buffer
 module HS = FStar.HyperStack
 module G = FStar.Ghost
 module L = FStar.List.Tot

diff --git a/test/LinkedList2.fst b/test/LinkedList2.fst
@@ -4,7 +4,6 @@ module B = FStar.Buffer
 module CN = C.Nullity
 module HS = FStar.HyperStack
 module G = FStar.Ghost
-module L = FStar.List.Tot
 module U32 = FStar.UInt32
 module MO = FStar.Modifies
 

diff --git a/test/LinkedList3.fst b/test/LinkedList3.fst
@@ -4,7 +4,6 @@ open LowStar.BufferOps
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
 module G = FStar.Ghost
-module L = FStar.List.Tot
 module U32 = FStar.UInt32
 module MO = LowStar.Modifies
 

diff --git a/test/Lowlevel.fst b/test/Lowlevel.fst
@@ -7,7 +7,6 @@ open FStar.UInt
 open FStar.HyperStack.ST
 
 module B = LowStar.Buffer
-module M = LowStar.Modifies
 module U16 = FStar.UInt16
 module U32 = FStar.UInt32
 

diff --git a/test/MutualStruct.fst b/test/MutualStruct.fst
@@ -5,7 +5,6 @@ open FStar.HyperStack.ST
 
 module U64 = FStar.UInt64
 module U8 = FStar.UInt8
-module SZ = FStar.SizeT
 
 let main () = C.EXIT_SUCCESS // dummy
 

diff --git a/test/NoShadow.fst b/test/NoShadow.fst
@@ -2,7 +2,6 @@ module NoShadow
 
 module U32 = FStar.UInt32
 module U64 = FStar.UInt64
-module HS = FStar.HyperStack
 
 open FStar.HyperStack.ST
 

diff --git a/test/Rust6.fst b/test/Rust6.fst
@@ -4,7 +4,6 @@ open FStar.HyperStack.ST
 
 module B = LowStar.Buffer
 module C = LowStar.ConstBuffer
-module HS = FStar.HyperStack
 
 
 inline_for_extraction noextract

diff --git a/test/Scope.fst b/test/Scope.fst
@@ -5,7 +5,6 @@ open FStar.Int32
 open FStar.HyperStack.ST
 open TestLib
 
-module B = FStar.Buffer
 
 let foo (): Stack bool (fun _ -> true) (fun h0 _ h1 -> h0 == h1) =
   true

diff --git a/test/TotalLoops.fst b/test/TotalLoops.fst
@@ -3,8 +3,6 @@ module TotalLoops
 open FStar
 open FStar.Buffer
 open FStar.HyperStack.ST
-module UInt32 = FStar.UInt32
-module UInt64 = FStar.UInt64
 
 let rec fib
   (x: nat)

diff --git a/test/Underspec.fst b/test/Underspec.fst
@@ -1,7 +1,6 @@
 module Underspec
 
 open FStar.HyperStack.ST
-module U32 = FStar.UInt32
 
 (* Checking that the *_underspec operators actually extract and run
 properly. *)

diff --git a/test/hello-system/SystemNative.fsti b/test/hello-system/SystemNative.fsti
@@ -13,7 +13,6 @@ module SystemNative
 module S = FStar.Seq
 module B = FStar.Buffer
 module U8 = FStar.UInt8
-module I32 = FStar.UInt8
 module U32 = FStar.UInt32
 
 (* Strings *******************************************************************)

diff --git a/test/sepcomp/b/B.fst b/test/sepcomp/b/B.fst
@@ -1,5 +1,4 @@
 module B
-module U32 = FStar.UInt32
 module U64 = FStar.UInt64
 module Cast = FStar.Int.Cast
 module A = A.Top

diff --git a/test/sepcomp/b/D.fst b/test/sepcomp/b/D.fst
@@ -1,5 +1,4 @@
 module D
-module U32 = FStar.UInt32
 module U64 = FStar.UInt64
 module Cast = FStar.Int.Cast
 module A = A.Top