From ff1abd02167d56994e7a838c5e2585d65d3cc39f Mon Sep 17 00:00:00 2001
From: Jean-Marie Madiot <jean-marie.madiot@inria.fr>
Date: Thu, 22 May 2025 15:09:26 +0200
Subject: [PATCH] oStdlib->Stdlib
---
coq-osiris/examples/proofs/bst.v | 2 +-
coq-osiris/examples/proofs/exceptions.v | 2 +-
coq-osiris/examples/proofs/exceptions_pure.v | 2 +-
coq-osiris/examples/proofs/inversion.v | 2 +-
coq-osiris/examples/proofs/iter.v | 2 +-
coq-osiris/examples/proofs/localstate.v | 2 +-
coq-osiris/examples/proofs/mem.v | 2 +-
coq-osiris/examples/proofs/merge.v | 2 +-
coq-osiris/examples/proofs/shiftreset.v | 2 +-
coq-osiris/examples/proofs/splay.v | 2 +-
coq-osiris/interp/extracted/dune | 2 +-
coq-osiris/interp/extracted/extract.v | 4 ++--
coq-osiris/interp/extracted/remove_generated_ml_files.sh | 2 +-
coq-osiris/theories/semantics/run.v | 2 +-
coq-osiris/theories/stdlib/{oStdlib.v => Stdlib.v} | 0
15 files changed, 15 insertions(+), 15 deletions(-)
rename coq-osiris/theories/stdlib/{oStdlib.v => Stdlib.v} (100%)
diff --git a/coq-osiris/examples/proofs/bst.v b/coq-osiris/examples/proofs/bst.v
index 95c1d7c4..9db17603 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 fc2f11a4..8739c3ed 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 5514f7a2..451fd6dc 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 184dcddc..ae9e26e3 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 27d6d10f..6d357d74 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 d560ed3f..4b1cc9be 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 e4dd39a7..3dc7b104 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 32c72b55..7d5c73d3 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 fee9b4c9..b4f70f56 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 9e5e896d..3cc92a27 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 cb92c4ca..5d3fd2b1 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 dd9201a5..4ac055b4 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 75c0600b..190eb4d0 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 cfcd3d4b..1064090a 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
--
GitLab