diff --git a/coq-osiris/examples/proofs/bst.v b/coq-osiris/examples/proofs/bst.v
index 95c1d7c4f262c9e5c96c44d2aa6534297b8be462..9db176039aca5f8fe96b3ff0a787d785c1f9b008 100644
--- a/coq-osiris/examples/proofs/bst.v
+++ b/coq-osiris/examples/proofs/bst.v
@@ -1,7 +1,7 @@
 Require Import Coq.Wellfounded.Inverse_Image.
 From osiris.logic Require Import orders sorting.
 From osiris Require Import osiris.
-From osiris.stdlib Require Import oStdlib.
+From osiris.stdlib Require Import Stdlib.
 From osiris.examples Require Import og_bst.
 
 (* -------------------------------------------------------------------------- *)
diff --git a/coq-osiris/examples/proofs/exceptions.v b/coq-osiris/examples/proofs/exceptions.v
index fc2f11a42368c6dac8fa19d536e1ab6b3d8d9f01..8739c3edb3520b43c1a797cac2957180012ae5ab 100644
--- a/coq-osiris/examples/proofs/exceptions.v
+++ b/coq-osiris/examples/proofs/exceptions.v
@@ -3,7 +3,7 @@ From iris.bi Require Import weakestpre.
 From iris Require Import base_logic.lib.gen_heap.
 
 From osiris Require Import osiris.
-From osiris.stdlib Require Import oStdlib.
+From osiris.stdlib Require Import Stdlib.
 From osiris.examples Require Import og_exception.
 
 (* TODO: We manually add exceptions to the environment. *)
diff --git a/coq-osiris/examples/proofs/exceptions_pure.v b/coq-osiris/examples/proofs/exceptions_pure.v
index 5514f7a2e93bcc798c9e66edb16799121c932ebc..451fd6dc12180c873bfa2f54d7c93083f254cdbe 100644
--- a/coq-osiris/examples/proofs/exceptions_pure.v
+++ b/coq-osiris/examples/proofs/exceptions_pure.v
@@ -6,7 +6,7 @@ should not be considered idiomatic (for this see iter.v instead).
 TODO: avoid [simp] at least when [eval ...] does not reduce to a value / exn *)
 
 From osiris Require Import osiris.
-From osiris.stdlib Require Import oStdlib.
+From osiris.stdlib Require Import Stdlib.
 From osiris.examples Require Import og_exception.
 
 Definition stdlib_with_notfound :=
diff --git a/coq-osiris/examples/proofs/inversion.v b/coq-osiris/examples/proofs/inversion.v
index 184dcddc4d869e60b226ac53fde6ab148ccf3f77..ae9e26e3fca95242f0c75fb35ee121ba4a48e39b 100644
--- a/coq-osiris/examples/proofs/inversion.v
+++ b/coq-osiris/examples/proofs/inversion.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import base tactics classes environments.
 From iris.algebra Require Import excl_auth.
 
 From osiris Require Import osiris.
-From osiris.stdlib Require Import oStdlib.
+From osiris.stdlib Require Import Stdlib.
 From osiris.examples Require Import og_inversion.
 
 (* ========================================================================== *)
diff --git a/coq-osiris/examples/proofs/iter.v b/coq-osiris/examples/proofs/iter.v
index 27d6d10f776f5f05b1249bf31998b5c28c4f8d37..6d357d74b4bdabe1c03a0561f38ec5e49d6ffb42 100644
--- a/coq-osiris/examples/proofs/iter.v
+++ b/coq-osiris/examples/proofs/iter.v
@@ -3,7 +3,7 @@ From iris.bi Require Import weakestpre.
 From iris Require Import base_logic.lib.gen_heap.
 
 From osiris Require Import osiris.
-From osiris.stdlib Require Import oStdlib.
+From osiris.stdlib Require Import Stdlib.
 From osiris.examples Require Import og_iter.
 
 Require Import Coq.Wellfounded.Inverse_Image.
diff --git a/coq-osiris/examples/proofs/localstate.v b/coq-osiris/examples/proofs/localstate.v
index d560ed3f6542c1e183af3f9925968530f0d233ae..4b1cc9be1dcc68c172065fe6383c49768c1f64d7 100644
--- a/coq-osiris/examples/proofs/localstate.v
+++ b/coq-osiris/examples/proofs/localstate.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import base tactics classes environments.
 From iris.algebra Require Import excl_auth.
 
 From osiris Require Import osiris.
-From osiris.stdlib Require Import oStdlib.
+From osiris.stdlib Require Import Stdlib.
 From osiris.examples Require Import og_localstate.
 
 (* ========================================================================== *)
diff --git a/coq-osiris/examples/proofs/mem.v b/coq-osiris/examples/proofs/mem.v
index e4dd39a7a2a0e4fa4edf6fa7c869618743f78f90..3dc7b10460db6561b9e7b34f7eeda12c09eaaeb3 100644
--- a/coq-osiris/examples/proofs/mem.v
+++ b/coq-osiris/examples/proofs/mem.v
@@ -3,7 +3,7 @@ From iris.bi Require Import weakestpre.
 From iris Require Import base_logic.lib.gen_heap.
 
 From osiris Require Import osiris.
-From osiris.stdlib Require Import oStdlib.
+From osiris.stdlib Require Import Stdlib.
 From osiris.examples Require Import og_mem.
 
 
diff --git a/coq-osiris/examples/proofs/merge.v b/coq-osiris/examples/proofs/merge.v
index 32c72b55ae94eaf59b864f83cd81c60eb43d9c2e..7d5c73d325668eaca341132620cafacf6b0614e6 100644
--- a/coq-osiris/examples/proofs/merge.v
+++ b/coq-osiris/examples/proofs/merge.v
@@ -1,7 +1,7 @@
 Require Import Coq.Wellfounded.Inverse_Image.
 From osiris.logic Require Import orders sorting.
 From osiris Require Import osiris.
-From osiris.stdlib Require Import oStdlib.
+From osiris.stdlib Require Import Stdlib.
 From osiris.logic Require Import sorting.
 From osiris.examples Require Import og_merge.
 
diff --git a/coq-osiris/examples/proofs/shiftreset.v b/coq-osiris/examples/proofs/shiftreset.v
index fee9b4c92640dad474aa93b05704154df2d745c4..b4f70f5668fc4528a5724b93b2484066880ceb4e 100644
--- a/coq-osiris/examples/proofs/shiftreset.v
+++ b/coq-osiris/examples/proofs/shiftreset.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import base tactics classes environments.
 From iris.algebra Require Import excl_auth.
 
 From osiris Require Import osiris.
-From osiris.stdlib Require Import oStdlib.
+From osiris.stdlib Require Import Stdlib.
 From osiris.examples Require Import og_shiftreset.
 
 (* Reasoning about delimited control via [shift/reset].
diff --git a/coq-osiris/examples/proofs/splay.v b/coq-osiris/examples/proofs/splay.v
index 9e5e896d53dfe072b7b10dfba15848f71b6ea969..3cc92a279bf4f237245b6b3be8439d43c57492a0 100644
--- a/coq-osiris/examples/proofs/splay.v
+++ b/coq-osiris/examples/proofs/splay.v
@@ -1,6 +1,6 @@
 From osiris.logic Require Import orders sorting.
 From osiris Require Import osiris.
-From osiris.stdlib Require Import oStdlib.
+From osiris.stdlib Require Import Stdlib.
 From osiris.examples Require Import og_splay.
 
 (* The algebraic data types of ['a tree] and ['a zipper]. *)
diff --git a/coq-osiris/interp/extracted/dune b/coq-osiris/interp/extracted/dune
index cb92c4ca2ab17919b798cad953092bc9175e77df..5d3fd2b151fd712a97058e5d642c505af40b3078 100644
--- a/coq-osiris/interp/extracted/dune
+++ b/coq-osiris/interp/extracted/dune
@@ -12,6 +12,6 @@
     BinPos BinNat Ascii BinInt ZArith_dec String Zpower option numbers list0
     countable void infinite fin_sets fin_maps mapset gmap locations PrimFloat
     Coqlib Zbits Integers int syntax sugar outcome code Mergesort options
-    eval_strat eval step DecimalString Externals oStdlib run
+    eval_strat eval step DecimalString Externals Stdlib run
  )
 )
diff --git a/coq-osiris/interp/extracted/extract.v b/coq-osiris/interp/extracted/extract.v
index dd9201a5e4cd66e1d1b254c27ac6c4c93c89a48b..4ac055b4b428d548d31a7b7ddafa5ead14b2ba52 100644
--- a/coq-osiris/interp/extracted/extract.v
+++ b/coq-osiris/interp/extracted/extract.v
@@ -1,6 +1,6 @@
 From Coq Require Import Extraction String Ascii.
 From osiris.semantics Require options eval_strat run.
-From osiris.stdlib Require Import oStdlib Externals.
+From osiris.stdlib Require Import Stdlib Externals.
 
 (* Suppress warnings of the form "Warning: The identifier Externals__eq contains
    __ which is reserved for the extraction" *)
@@ -30,6 +30,6 @@ Separate Extraction
   sugar
   run
   eval_strat
-  oStdlib
+  Stdlib
   options
 .
diff --git a/coq-osiris/interp/extracted/remove_generated_ml_files.sh b/coq-osiris/interp/extracted/remove_generated_ml_files.sh
index 75c0600b9fddf4f047a5dc97b9531a64a8de9665..190eb4d03f736f163a32babbb01b43157b61aee4 100755
--- a/coq-osiris/interp/extracted/remove_generated_ml_files.sh
+++ b/coq-osiris/interp/extracted/remove_generated_ml_files.sh
@@ -55,7 +55,7 @@ DecimalString.ml      DecimalString.mli      \
 example_list.ml       example_list.mli       \
 interp_det_stepto.ml  interp_det_stepto.mli  \
 interp_pure_stepto.ml interp_pure_stepto.mli \
-oStdlib.ml            oStdlib.mli            \
+Stdlib.ml             Stdlib.mli             \
 eval_det.ml           eval_det.mli           \
 eval_strat.ml         eval_strat.mli         \
 run.ml                run.mli                \
diff --git a/coq-osiris/theories/semantics/run.v b/coq-osiris/theories/semantics/run.v
index cfcd3d4bc0ee0faaf6e7e504c5181c8ba2758032..1064090abcd08f03e1269d7d243649f4ae9b15cb 100644
--- a/coq-osiris/theories/semantics/run.v
+++ b/coq-osiris/theories/semantics/run.v
@@ -2,7 +2,7 @@ From stdpp Require Import gmap.
 From osiris Require Import base.
 From osiris.lang Require Import syntax locations sugar.
 From osiris.semantics Require Import code step options eval_strat.
-From osiris.stdlib Require Import oStdlib.
+From osiris.stdlib Require Import Stdlib.
 
 (** Perform one step of confluent parallel reductions or returns [None] if there
 is no trivially confluent step. It is used to can eliminate a large part of the
diff --git a/coq-osiris/theories/stdlib/oStdlib.v b/coq-osiris/theories/stdlib/Stdlib.v
similarity index 100%
rename from coq-osiris/theories/stdlib/oStdlib.v
rename to coq-osiris/theories/stdlib/Stdlib.v